let L be TopSpace; :: thesis: for G, G1 being Subset-Family of L st G is Cover of L & G is finite holds
for ALL being set st G1 = G \ { X where X is Subset of L : ( X in G & ex Y being Subset of L st
( Y in G & X c< Y ) ) } & ALL = { C where C is Subset-Family of L : ( C is Cover of L & C c= G1 ) } holds
ALL has_lower_Zorn_property_wrt RelIncl ALL
let G, G1 be Subset-Family of L; :: thesis: ( G is Cover of L & G is finite implies for ALL being set st G1 = G \ { X where X is Subset of L : ( X in G & ex Y being Subset of L st
( Y in G & X c< Y ) ) } & ALL = { C where C is Subset-Family of L : ( C is Cover of L & C c= G1 ) } holds
ALL has_lower_Zorn_property_wrt RelIncl ALL )
assume that
A1: G is Cover of L and
A2: G is finite ; :: thesis: for ALL being set st G1 = G \ { X where X is Subset of L : ( X in G & ex Y being Subset of L st
( Y in G & X c< Y ) ) } & ALL = { C where C is Subset-Family of L : ( C is Cover of L & C c= G1 ) } holds
ALL has_lower_Zorn_property_wrt RelIncl ALL
let ALL be set ; :: thesis: ( G1 = G \ { X where X is Subset of L : ( X in G & ex Y being Subset of L st
( Y in G & X c< Y ) ) } & ALL = { C where C is Subset-Family of L : ( C is Cover of L & C c= G1 ) } implies ALL has_lower_Zorn_property_wrt RelIncl ALL )
set ZAW = { X where X is Subset of L : ( X in G & ex Y being Subset of L st
( Y in G & X c< Y ) ) } ;
assume that
A3: G1 = G \ { X where X is Subset of L : ( X in G & ex Y being Subset of L st
( Y in G & X c< Y ) ) } and
A4: ALL = { C where C is Subset-Family of L : ( C is Cover of L & C c= G1 ) } ; :: thesis: ALL has_lower_Zorn_property_wrt RelIncl ALL
A5: G1 is Cover of L by A1, A2, A3, Th45;
set R = RelIncl ALL;
A6: field (RelIncl ALL) = ALL by WELLORD2:def 1;
let Y be set ; :: according to ORDERS_1:def 11 :: thesis: ( not Y c= ALL or not (RelIncl ALL) |_2 Y is being_linear-order or ex b1 being set st
( b1 in ALL & ( for b2 being set holds
( not b2 in Y or [b1,b2] in RelIncl ALL ) ) ) )
assume that
A7: Y c= ALL and
A8: (RelIncl ALL) |_2 Y is being_linear-order ; :: thesis: ex b1 being set st
( b1 in ALL & ( for b2 being set holds
( not b2 in Y or [b1,b2] in RelIncl ALL ) ) )
per cases ( not Y is empty or Y is empty ) ;
suppose A9: not Y is empty ; :: thesis: ex b1 being set st
( b1 in ALL & ( for b2 being set holds
( not b2 in Y or [b1,b2] in RelIncl ALL ) ) )
defpred S2[ set ] means ( not $1 is empty implies meet $1 in Y );
set E = { H1(D) where D is Subset-Family of L : D in bool G1 } ;
take x = meet Y; :: thesis: ( x in ALL & ( for b1 being set holds
( not b1 in Y or [x,b1] in RelIncl ALL ) ) )
A10: ALL c= { H1(D) where D is Subset-Family of L : D in bool G1 }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ALL or a in { H1(D) where D is Subset-Family of L : D in bool G1 } )
assume a in ALL ; :: thesis: a in { H1(D) where D is Subset-Family of L : D in bool G1 }
then ex C being Subset-Family of L st
( a = C & C is Cover of L & C c= G1 ) by A4;
hence a in { H1(D) where D is Subset-Family of L : D in bool G1 } ; :: thesis: verum
end;
A11: bool G1 is finite by A2, A3;
{ H1(D) where D is Subset-Family of L : D in bool G1 } is finite from FRAENKEL:sch 21(A11);
then A12: Y is finite by A7, A10;
A13: for x, B being set st x in Y & B c= Y & S2[B] holds
S2[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in Y & B c= Y & S2[B] implies S2[B \/ {x}] )
assume that
A14: x in Y and
B c= Y and
A15: S2[B] and
not B \/ {x} is empty ; :: thesis: meet (B \/ {x}) in Y
per cases ( B is empty or not B is empty ) ;
suppose A16: not B is empty ; :: thesis: meet (B \/ {x}) in Y
(RelIncl ALL) |_2 Y is connected by A8;
then A17: (RelIncl ALL) |_2 Y is_connected_in field ((RelIncl ALL) |_2 Y) ;
field ((RelIncl ALL) |_2 Y) = Y by A6, A7, ORDERS_1:71;
then ( [x,(meet B)] in (RelIncl ALL) |_2 Y or [(meet B),x] in (RelIncl ALL) |_2 Y or x = meet B ) by A14, A15, A16, A17;
then ( [x,(meet B)] in RelIncl ALL or [(meet B),x] in RelIncl ALL or x = meet B ) by XBOOLE_0:def 4;
then A18: ( meet B c= x or x c= meet B ) by A7, A14, A15, A16, WELLORD2:def 1;
meet (B \/ {x}) = (meet B) /\ (meet {x}) by A16, SETFAM_1:9
.= (meet B) /\ x by SETFAM_1:10 ;
hence meet (B \/ {x}) in Y by A14, A15, A16, A18, XBOOLE_1:28; :: thesis: verum
end;
end;
end;
consider y being object such that
A19: y in Y by A9;
y in ALL by A7, A19;
then A20: ex C being Subset-Family of L st
( y = C & C is Cover of L & C c= G1 ) by A4;
then reconsider X = x as Subset-Family of L by A19, SETFAM_1:7;
A21: S2[ {} ] ;
A22: S2[Y] from FINSET_1:sch 2(A12, A21, A13);
A23: X is Cover of L
proof
let a be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not a in the carrier of L or a in union X )
assume A24: a in the carrier of L ; :: thesis: a in union X
meet Y in ALL by A7, A9, A22;
then consider C being Subset-Family of L such that
A25: meet Y = C and
A26: C is Cover of L and
C c= G1 by A4;
the carrier of L c= union C by A26, SETFAM_1:def 11;
hence a in union X by A24, A25; :: thesis: verum
end;
x c= G1 by A19, A20, SETFAM_1:7;
hence A27: x in ALL by A4, A23; :: thesis: for b1 being set holds
( not b1 in Y or [x,b1] in RelIncl ALL )
let y be set ; :: thesis: ( not y in Y or [x,y] in RelIncl ALL )
assume A28: y in Y ; :: thesis: [x,y] in RelIncl ALL
then x c= y by SETFAM_1:7;
hence [x,y] in RelIncl ALL by A7, A27, A28, WELLORD2:def 1; :: thesis: verum
end;
suppose A29: Y is empty ; :: thesis: ex b1 being set st
( b1 in ALL & ( for b2 being set holds
( not b2 in Y or [b1,b2] in RelIncl ALL ) ) )
take G1 ; :: thesis: ( G1 in ALL & ( for b1 being set holds
( not b1 in Y or [G1,b1] in RelIncl ALL ) ) )
thus ( G1 in ALL & ( for b1 being set holds
( not b1 in Y or [G1,b1] in RelIncl ALL ) ) ) by A4, A5, A29; :: thesis: verum
end;
end;