let T be 1-sorted ; :: thesis: for F being finite Subset-Family of T
for F1 being Subset-Family of T st F is Cover of T & F1 = F \ { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } holds
F1 is Cover of T
let F be finite Subset-Family of T; :: thesis: for F1 being Subset-Family of T st F is Cover of T & F1 = F \ { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } holds
F1 is Cover of T
let F1 be Subset-Family of T; :: thesis: ( F is Cover of T & F1 = F \ { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } implies F1 is Cover of T )
assume that
A1: the carrier of T c= union F and
A2: F1 = F \ { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } ; :: according to SETFAM_1:def 12 :: thesis: F1 is Cover of T
set ZAW = { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } ;
thus the carrier of T c= union F1 :: according to SETFAM_1:def 12 :: thesis: verum

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in the carrier of T or t in union F1 )
assume t in the carrier of T ; :: thesis: t in union F1
then consider Z being set such that
A3: t in Z and
A4: Z in F by A1, TARSKI:def 4;
set ALL = { X where X is Subset of T : ( Z c< X & X in F ) } ;

per cases ( { X where X is Subset of T : ( Z c< X & X in F ) } is empty or not { X where X is Subset of T : ( Z c< X & X in F ) } is empty ) ;

suppose A5: { X where X is Subset of T : ( Z c< X & X in F ) } is empty ; :: thesis: t in union F1

now

assume Z in { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } ; :: thesis: contradiction
then consider X being Subset of T such that
A6: Z = X and
X in F and
A7: ex Y being Subset of T st
( Y in F & X c< Y ) ;
consider Y being Subset of T such that
A8: ( Y in F & X c< Y ) by A7;
Y in { X where X is Subset of T : ( Z c< X & X in F ) } by A6, A8;
hence contradiction by A5; :: thesis: verum

end;

then Z in F1 by A2, A4, XBOOLE_0:def 5;
hence t in union F1 by A3, TARSKI:def 4; :: thesis: verum

end;

suppose not { X where X is Subset of T : ( Z c< X & X in F ) } is empty ; :: thesis: t in union F1

then consider w being set such that
A9: w in { X where X is Subset of T : ( Z c< X & X in F ) } by XBOOLE_0:def 1;
consider R being Relation of { X where X is Subset of T : ( Z c< X & X in F ) } such that
A10: for x, y being set holds
( [x,y] in R iff ( x in { X where X is Subset of T : ( Z c< X & X in F ) } & y in { X where X is Subset of T : ( Z c< X & X in F ) } & S₁[x,y] ) ) from RELSET_1:sch 1();
A11: R is_reflexive_in { X where X is Subset of T : ( Z c< X & X in F ) }

proof

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in { X where X is Subset of T : ( Z c< X & X in F ) } or [x,x] in R )
thus ( not x in { X where X is Subset of T : ( Z c< X & X in F ) } or [x,x] in R ) by A10; :: thesis: verum

end;

then A12: field R = { X where X is Subset of T : ( Z c< X & X in F ) } by ORDERS_1:98;
A13: R partially_orders { X where X is Subset of T : ( Z c< X & X in F ) }

proof

thus R is_reflexive_in { X where X is Subset of T : ( Z c< X & X in F ) } by A11; :: according to ORDERS_1:def 7 :: thesis: ( R is_transitive_in { X where X is Subset of T : ( Z c< X & X in F ) } & R is_antisymmetric_in { X where X is Subset of T : ( Z c< X & X in F ) } )
thus R is_transitive_in { X where X is Subset of T : ( Z c< X & X in F ) } :: thesis: R is_antisymmetric_in { X where X is Subset of T : ( Z c< X & X in F ) }

proof

let x, y, z be set ; :: according to RELAT_2:def 8 :: thesis: ( not x in { X where X is Subset of T : ( Z c< X & X in F ) } or not y in { X where X is Subset of T : ( Z c< X & X in F ) } or not z in { X where X is Subset of T : ( Z c< X & X in F ) } or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that
A14: x in { X where X is Subset of T : ( Z c< X & X in F ) } and
y in { X where X is Subset of T : ( Z c< X & X in F ) } and
A15: z in { X where X is Subset of T : ( Z c< X & X in F ) } ; :: thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R )
assume ( [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
then ( x c= y & y c= z ) by A10;
then x c= z by XBOOLE_1:1;
hence [x,z] in R by A10, A14, A15; :: thesis: verum

end;

let x, y be set ; :: according to RELAT_2:def 4 :: thesis: ( not x in { X where X is Subset of T : ( Z c< X & X in F ) } or not y in { X where X is Subset of T : ( Z c< X & X in F ) } or not [x,y] in R or not [y,x] in R or x = y )
assume that
x in { X where X is Subset of T : ( Z c< X & X in F ) } and
y in { X where X is Subset of T : ( Z c< X & X in F ) } ; :: thesis: ( not [x,y] in R or not [y,x] in R or x = y )
assume ( [x,y] in R & [y,x] in R ) ; :: thesis: x = y
hence ( x c= y & y c= x ) by A10; :: according to XBOOLE_0:def 10 :: thesis: verum

end;

A16: R is reflexive by A11, A12, RELAT_2:def 9;
{ X where X is Subset of T : ( Z c< X & X in F ) } has_upper_Zorn_property_wrt R

proof

let Y be set ; :: according to ORDERS_1:def 9 :: thesis: ( not Y c= { X where X is Subset of T : ( Z c< X & X in F ) } or not R |_2 Y is being_linear-order or ex b₁ being set st
( b₁ in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b₂ being set holds
( not b₂ in Y or [b₂,b₁] in R ) ) ) )
assume that
A17: Y c= { X where X is Subset of T : ( Z c< X & X in F ) } and
A18: R |_2 Y is being_linear-order ; :: thesis: ex b₁ being set st
( b₁ in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b₂ being set holds
( not b₂ in Y or [b₂,b₁] in R ) ) )

per cases ( not Y is empty or Y is empty ) ;

suppose A19: not Y is empty ; :: thesis: ex b₁ being set st
( b₁ in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b₂ being set holds
( not b₂ in Y or [b₂,b₁] in R ) ) )

defpred S₂[ set ] means ( not $1 is empty & $1 c= Y implies union $1 in Y );
take union Y ; :: thesis: ( union Y in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b₁ being set holds
( not b₁ in Y or [b₁,(union Y)] in R ) ) )
A20: S₂[ {} ] ;
A21: for A, B being set st A in Y & B in Y holds
A \/ B in Y

proof

A22: R |_2 Y c= R by XBOOLE_1:17;
R |_2 Y is connected by A18, ORDERS_1:def 5;
then A23: R |_2 Y is_connected_in field (R |_2 Y) by RELAT_2:def 14;
let A, B be set ; :: thesis: ( A in Y & B in Y implies A \/ B in Y )
assume A24: ( A in Y & B in Y ) ; :: thesis: A \/ B in Y
field (R |_2 Y) = Y by A12, A16, A17, ORDERS_1:181;
then ( [A,B] in R |_2 Y or [B,A] in R |_2 Y or A = B ) by A24, A23, RELAT_2:def 6;
then ( A c= B or B c= A ) by A10, A22;
hence A \/ B in Y by A24, XBOOLE_1:12; :: thesis: verum

end;

A25: 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: ( x in Y & B c= Y & S₂[B] implies S₂[B \/ {x}] )
assume that
A26: x in Y and
A27: ( B c= Y & S₂[B] ) and
not B \/ {x} is empty and
B \/ {x} c= Y ; :: thesis: union (B \/ {x}) in Y
A28: union {x} = x by ZFMISC_1:31;

per cases ( B is empty or not B is empty ) ;

suppose B is empty ; :: thesis: union (B \/ {x}) in Y

hence union (B \/ {x}) in Y by A26, ZFMISC_1:31; :: thesis: verum

end;

suppose not B is empty ; :: thesis: union (B \/ {x}) in Y

then x \/ (union B) in Y by A21, A26, A27;
hence union (B \/ {x}) in Y by A28, ZFMISC_1:96; :: thesis: verum

end;

end;

end;

consider y being set such that
A29: y in Y by A19, XBOOLE_0:def 1;
y in { X where X is Subset of T : ( Z c< X & X in F ) } by A17, A29;
then consider X being Subset of T such that
A30: X = y and
A31: Z c< X and
X in F ;
A32: X c= union Y by A29, A30, ZFMISC_1:92;
then A33: Z <> union Y by A31, XBOOLE_0:def 8;
Z c= X by A31, XBOOLE_0:def 8;
then Z c= union Y by A32, XBOOLE_1:1;
then A34: Z c< union Y by A33, XBOOLE_0:def 8;
A35: { X where X is Subset of T : ( Z c< X & X in F ) } c= F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { X where X is Subset of T : ( Z c< X & X in F ) } or x in F )
assume x in { X where X is Subset of T : ( Z c< X & X in F ) } ; :: thesis: x in F
then ex X being Subset of T st
( X = x & Z c< X & X in F ) ;
hence x in F ; :: thesis: verum

end;

then A36: Y c= F by A17, XBOOLE_1:1;
A37: Y is finite by A17, A35;
S₂[Y] from FINSET_1:sch 2(A37, A20, A25);
then union Y in F by A19, A36;
hence A38: union Y in { X where X is Subset of T : ( Z c< X & X in F ) } by A34; :: thesis: for b₁ being set holds
( not b₁ in Y or [b₁,(union Y)] in R )
let z be set ; :: thesis: ( not z in Y or [z,(union Y)] in R )
assume A39: z in Y ; :: thesis: [z,(union Y)] in R
then S₁[z, union Y] by ZFMISC_1:92;
hence [z,(union Y)] in R by A10, A17, A38, A39; :: thesis: verum

end;

suppose A40: Y is empty ; :: thesis: ex b₁ being set st
( b₁ in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b₂ being set holds
( not b₂ in Y or [b₂,b₁] in R ) ) )

take w ; :: thesis: ( w in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b₁ being set holds
( not b₁ in Y or [b₁,w] in R ) ) )
thus w in { X where X is Subset of T : ( Z c< X & X in F ) } by A9; :: thesis: for b₁ being set holds
( not b₁ in Y or [b₁,w] in R )
thus for b₁ being set holds
( not b₁ in Y or [b₁,w] in R ) by A40; :: thesis: verum

end;

end;

end;

then consider M being set such that
A41: M is_maximal_in R by A12, A13, ORDERS_1:173;
A42: M in field R by A41, ORDERS_1:def 11;
then A43: ex X being Subset of T st
( X = M & Z c< X & X in F ) by A12;

now

assume M in { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } ; :: thesis: contradiction
then consider H being Subset of T such that
A44: M = H and
H in F and
A45: ex Y being Subset of T st
( Y in F & H c< Y ) ;
consider Y being Subset of T such that
A46: Y in F and
A47: H c< Y by A45;
Z c< Y by A43, A44, A47, XBOOLE_1:56;
then A48: Y in { X where X is Subset of T : ( Z c< X & X in F ) } by A46;
H c= Y by A47, XBOOLE_0:def 8;
then [M,Y] in R by A10, A12, A42, A44, A48;
hence contradiction by A12, A41, A44, A47, A48, ORDERS_1:def 11; :: thesis: verum

end;

then A49: M in F1 by A2, A43, XBOOLE_0:def 5;
Z c= M by A43, XBOOLE_0:def 8;
hence t in union F1 by A3, A49, TARSKI:def 4; :: thesis: verum

end;

end;

end;

thus verum ; :: thesis: verum