reconsider F = bool X as Subset-Family of X ;
take F ; :: thesis: ( not F is empty & F is () )
thus not F is empty ; :: thesis: F is ()
let B be Subset of X; :: according to PROOFS_1:def 29 :: thesis: ( B in F iff for S being finite Subset of B holds S in F )
thus ( B in F implies for S being finite Subset of B holds S in F ) :: thesis: ( ( for S being finite Subset of B holds S in F ) implies B in F )

proof

assume B in F ; :: thesis: for S being finite Subset of B holds S in F
let S be finite Subset of B; :: thesis: S in F
( S c= B & B c= X ) ;
then S c= X ;
hence S in F ; :: thesis: verum

end;

assume for S being finite Subset of B holds S in F ; :: thesis: B in F
thus B in F ; :: thesis: verum