thus ( F is finite-character implies for B being Subset of X holds
( B in F iff for S being finite Subset of B holds S in F ) ) ; :: thesis: ( ( for B being Subset of X holds
( B in F iff for S being finite Subset of B holds S in F ) ) implies F is finite-character )
assume A1: for B being Subset of X holds
( B in F iff for S being finite Subset of B holds S in F ) ; :: thesis: F is finite-character
let Y be set ; :: according to PROOFS_1:def 28 :: thesis: ( Y in F iff for S being finite Subset of Y holds S in F )
thus ( Y in F implies for S being finite Subset of Y holds S in F ) by A1; :: thesis: ( ( for S being finite Subset of Y holds S in F ) implies Y in F )
assume A2: for S being finite Subset of Y holds S in F ; :: thesis: Y in F
Y c= X

proof

assume not Y c= X ; :: thesis: contradiction
then consider u being object such that
A4: u in Y and
A5: not u in X ;
{u} c= Y by A4, TARSKI:def 1;
then reconsider S = {u} as finite Subset of Y ;
S in F by A2;
then ( S c= X & u in S ) by TARSKI:def 1;
hence contradiction by A5; :: thesis: verum

end;

hence Y in F by A1, A2; :: thesis: verum