let X be non empty finite set ; :: thesis: for F being Full-family of X holds
( saturated-subsets F is (B1) & saturated-subsets F is (B2) )
let F be Full-family of X; :: thesis: ( saturated-subsets F is (B1) & saturated-subsets F is (B2) )
set ss = saturated-subsets F;
A1: Maximal_wrt F is (M1) by Th30;
then consider A9, B9 being Subset of X such that
A2: [A9,B9] >= [([#] X),([#] X)] and
A3: [A9,B9] in Maximal_wrt F by Def19;
[#] X c= B9 by A2, Th15;
then A4: [#] X = B9 by XBOOLE_0:def 10;
A9 ^|^ B9,F by A3, Def18;
then X in saturated-subsets F by A4;
hence saturated-subsets F is (B1) by Def4; :: thesis: saturated-subsets F is (B2)
thus saturated-subsets F is (B2) :: thesis: verum

proof

let a, b be set ; :: according to FINSUB_1:def 2 :: thesis: ( not a in saturated-subsets F or not b in saturated-subsets F or a /\ b in saturated-subsets F )
assume that
A5: a in saturated-subsets F and
A6: b in saturated-subsets F ; :: thesis: a /\ b in saturated-subsets F
reconsider a9 = a, b9 = b as Subset of X by A5, A6;
A7: Maximal_wrt F is (M3) by Th30;
consider B2, A2 being Subset of X such that
A8: b = B2 and
A9: A2 ^|^ B2,F by A6, Th33;
A10: [A2,B2] in Maximal_wrt F by A9, Def18;
consider B1, A1 being Subset of X such that
A11: a = B1 and
A12: A1 ^|^ B1,F by A5, Th33;
A13: [A1,B1] in Maximal_wrt F by A12, Def18;
consider A9, B9 being Subset of X such that
A14: [A9,B9] >= [(a9 /\ b9),(a9 /\ b9)] and
A15: [A9,B9] in Maximal_wrt F by A1, Def19;
A16: A9 c= a /\ b by A14, Th15;
a /\ b c= b by XBOOLE_1:17;
then A9 c= B2 by A8, A16, XBOOLE_1:1;
then A17: B9 c= B2 by A10, A15, A7, Def21;
A18: a /\ b c= B9 by A14, Th15;
a /\ b c= a by XBOOLE_1:17;
then A9 c= B1 by A11, A16, XBOOLE_1:1;
then B9 c= B1 by A13, A15, A7, Def21;
then B9 c= a /\ b by A11, A8, A17, XBOOLE_1:19;
then A19: B9 = a /\ b by A18, XBOOLE_0:def 10;
A9 ^|^ B9,F by A15, Def18;
hence a /\ b in saturated-subsets F by A19; :: thesis: verum

end;