FDL > PVS > Prelude > finite sets def > is_finite : const-decl

is_finite(S): bool = EXISTS N, (f:[(S) - > below[N]]) : injective?(f);