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