:: deftheorem defines finite-character PROOFS_1:def 29 :
for X being set
for F being Subset-Family of X holds
( F is finite-character iff for B being Subset of X holds
( B in F iff for S being finite Subset of B holds S in F ) );