:: deftheorem Def20r defines finite-character PROOFS_1:def 28 :
for X being set holds
( X is finite-character iff for Y being set holds
( Y in X iff for S being finite Subset of Y holds S in X ) );