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;
then A13: R is reflexive by A11, RELAT_2:def 9;
A14: 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 A15: ( 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 ) } & 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, 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 ( 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 ) } ) ; :: 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;

{ 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
A16: Y c= { X where X is Subset of T : ( Z c< X & X in F ) } and
A17: 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 A18: 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 ) ) )

then consider y being set such that
A19: y in Y by XBOOLE_0:def 1;
y in { X where X is Subset of T : ( Z c< X & X in F ) } by A16, A19;
then consider X being Subset of T such that
A20: X = y and
A21: Z c< X and
X in F ;
X: Z c= X by A21, XBOOLE_0:def 8;
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 ) ) )
A23: X c= union Y by A19, A20, ZFMISC_1:92;
then A24: Z c= union Y by X, XBOOLE_1:1;
A25: for A, B being set st A in Y & B in Y holds
A \/ B in Y

proof

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

end;

defpred S₂[ set ] means ( not $1 is empty & $1 c= Y implies union $1 in Y );
A30: { 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 A31: Y c= F by A16, XBOOLE_1:1;
A32: Y is finite by A16, A30;
A33: S₂[ {} ] ;
A34: 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
A35: x in Y and
A36: B c= Y and
A37: S₂[B] and
( not B \/ {x} is empty & B \/ {x} c= Y ) ; :: thesis: union (B \/ {x}) in Y
A38: 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 A35, ZFMISC_1:31; :: thesis: verum

end;

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

then x \/ (union B) in Y by A25, A35, A36, A37;
hence union (B \/ {x}) in Y by A38, ZFMISC_1:96; :: thesis: verum

end;

end;

end;

S₂[Y] from FINSET_1:sch 2(A32, A33, A34);
then A39: union Y in F by A18, A31;
Z <> union Y by A23, A21, XBOOLE_0:def 8;
then Z c< union Y by A24, XBOOLE_0:def 8;
hence A40: union Y in { X where X is Subset of T : ( Z c< X & X in F ) } by A39; :: 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 A41: 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, A16, A40, A41; :: thesis: verum

end;

suppose A42: 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 A42; :: thesis: verum

end;

end;

end;

then consider M being set such that
A43: M is_maximal_in R by A12, A14, ORDERS_1:173;
A44: M in field R by A43, ORDERS_1:def 11;
then A45: 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
A46: M = H and
H in F and
A47: ex Y being Subset of T st
( Y in F & H c< Y ) ;
consider Y being Subset of T such that
A48: Y in F and
A49: H c< Y by A47;
A51: Z c< Y by A45, A46, A49, XBOOLE_1:56;
X: H c= Y by A49, XBOOLE_0:def 8;
A52: Y in { X where X is Subset of T : ( Z c< X & X in F ) } by A48, A51;
then [M,Y] in R by A10, A12, A44, A46, X;
hence contradiction by A12, A43, A46, A49, A52, ORDERS_1:def 11; :: thesis: verum

end;

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

end;

end;

end;

thus verum ; :: thesis: verum