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 Th30;
then consider A', B' being Subset of such that
A2:
[A',B'] >= [([#] X),([#] X)]
and
A3:
[A',B'] in Maximal_wrt F
by Def19;
[#] X c= B'
by A2, Th15;
then A4:
[#] X = B'
by XBOOLE_0:def 10;
A' ^|^ B',F
by A3, Def18;
then
X in saturated-subsets F
by A4;
hence
saturated-subsets F is (B1)
by Def4; 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 a' =
a,
b' =
b as
Subset of
by A5, A6;
A7:
Maximal_wrt F is
(M3)
by Th30;
consider B2,
A2 being
Subset of
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
such that A11:
a = B1
and A12:
A1 ^|^ B1,
F
by A5, Th33;
A13:
[A1,B1] in Maximal_wrt F
by A12, Def18;
consider A',
B' being
Subset of
such that A14:
[A',B'] >= [(a' /\ b'),(a' /\ b')]
and A15:
[A',B'] in Maximal_wrt F
by A1, Def19;
A16:
A' c= a /\ b
by A14, Th15;
a /\ b c= b
by XBOOLE_1:17;
then
A' c= B2
by A8, A16, XBOOLE_1:1;
then A17:
B' c= B2
by A10, A15, A7, Def21;
A18:
a /\ b c= B'
by A14, Th15;
a /\ b c= a
by XBOOLE_1:17;
then
A' c= B1
by A11, A16, XBOOLE_1:1;
then
B' c= B1
by A13, A15, A7, Def21;
then
B' c= a /\ b
by A11, A8, A17, XBOOLE_1:19;
then A19:
B' = a /\ b
by A18, XBOOLE_0:def 10;
A' ^|^ B',
F
by A15, Def18;
hence
a /\ b in saturated-subsets F
by A19;
verum
end;