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 Th28;
then consider A9, B9 being Subset of X such that
A2: [A9,B9] >= [([#] X),([#] X)] and
A3: [A9,B9] in Maximal_wrt F ;
[#] X c= B9 by A2;
then A4: [#] X = B9 by XBOOLE_0:def 10;
A9 ^|^ B9,F by A3;
then X in saturated-subsets F by A4;
hence saturated-subsets F is (B1) ; :: 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 Th28;
consider B2, A2 being Subset of X such that
A8: b = B2 and
A9: A2 ^|^ B2,F by A6, Th31;
A10: [A2,B2] in Maximal_wrt F by A9;
consider B1, A1 being Subset of X such that
A11: a = B1 and
A12: A1 ^|^ B1,F by A5, Th31;
A13: [A1,B1] in Maximal_wrt F by A12;
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;
A16: A9 c= a /\ b by A14;
a /\ b c= b by XBOOLE_1:17;
then A9 c= B2 by A8, A16;
then A17: B9 c= B2 by A10, A15, A7;
A18: a /\ b c= B9 by A14;
a /\ b c= a by XBOOLE_1:17;
then A9 c= B1 by A11, A16;
then B9 c= B1 by A13, A15, A7;
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;
hence a /\ b in saturated-subsets F by A19; :: thesis: verum

end;