let X be non empty finite set ; 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; ( 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)
; saturated-subsets F is (B2)
thus
saturated-subsets F is (B2)
verumproof
let a,
b be
set ;
FINSUB_1:def 2 ( 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
;
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;
verum
end;