:: deftheorem Def20 defines finite-character PROOFS_1:def 27 :
for X being set holds
( X is finite-character iff for a being object holds
( a in X iff ex B being set st
( B = a & ( for S being finite Subset of B holds S in X ) ) ) );