let L be TopSpace; :: thesis:
let G, G1 be Subset-Family of L; :: thesis:
assume that
A1: G is Cover of L and
A2: G is finite ; :: thesis:
let ALL be set ; :: thesis:
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:
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:
assume that
A7: Y c= ALL and
A8: (RelIncl ALL) |_2 Y is being_linear-order ; :: thesis:

per cases ;

suppose A9: not Y is empty ; :: thesis:

defpred S₂[ set ] means ( not $1 is empty implies meet $1 in Y );
set E = { H₁(D) where D is Subset-Family of L : D in bool G1 } ;
take x = meet Y; :: thesis:
A10: ALL c= { H₁(D) where D is Subset-Family of L : D in bool G1 }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in ALL ; :: thesis:
then ex C being Subset-Family of L st
( a = C & C is Cover of L & C c= G1 ) by A4;
hence a in { H₁(D) where D is Subset-Family of L : D in bool G1 } ; :: thesis:

end;

A11: bool G1 is finite by A2, A3;
{ H₁(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 & S₂[B] holds
S₂[B \/ {x}]

proof

let x, B be set ; :: thesis:
assume that
A14: x in Y and
B c= Y and
A15: S₂[B] and
not B \/ {x} is empty ; :: thesis:

per cases ;

suppose B is empty ; :: thesis:

hence meet (B \/ {x}) in Y by A14, SETFAM_1:10; :: thesis:

end;

suppose A16: not B is empty ; :: thesis:

(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:

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: S₂[ {} ] ;
A22: S₂[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:
assume A24: a in the carrier of L ; :: thesis:
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:

end;

x c= G1 by A19, A20, SETFAM_1:7;
hence A27: x in ALL by A4, A23; :: thesis:
let y be set ; :: thesis:
assume A28: y in Y ; :: thesis:
then x c= y by SETFAM_1:7;
hence [x,y] in RelIncl ALL by A7, A27, A28, WELLORD2:def 1; :: thesis:

end;

suppose A29: Y is empty ; :: thesis:

take G1 ; :: thesis:
thus ( G1 in ALL & ( for b₁ being set holds
( not b₁ in Y or [G1,b₁] in RelIncl ALL ) ) ) by A4, A5, A29; :: thesis:

end;

end;