let X be set ; :: thesis: bool X is Field_Subset of X
reconsider K = bool X as Subset-Family of X ;
A1: K is cap-closed

proof

let A, B be set ; :: according to FINSUB_1:def 2 :: thesis: ( not A in K or not B in K or A /\ B in K )
assume that
A2: A in K and
B in K ; :: thesis: A /\ B in K
A /\ B c= X by A2, XBOOLE_1:108;
hence A /\ B in K ; :: thesis: verum

end;

K is compl-closed

proof

let A be Subset of X; :: according to PROB_1:def 1 :: thesis: ( A in K implies A ` in K )
assume A in K ; :: thesis: A ` in K
thus A ` in K ; :: thesis: verum

end;

hence bool X is Field_Subset of X by A1; :: thesis: verum