let X be set ; :: thesis: ( X is c=-linear implies ex Y being set st
( Y c= X & union Y = union X & ( for Z being set st Z c= Y & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) ) )
assume A1: X is c=-linear ; :: thesis: ex Y being set st
( Y c= X & union Y = union X & ( for Z being set st Z c= Y & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )
consider R being Relation such that
A2: R well_orders X by WELLORD2:17;
A3: R |_2 X is well-ordering by A2, WELLORD2:16;
A4: field (R |_2 X) = X by A2, WELLORD2:16;
R |_2 X, RelIncl (order_type_of (R |_2 X)) are_isomorphic by A3, WELLORD2:def 2;
then RelIncl (order_type_of (R |_2 X)),R |_2 X are_isomorphic by WELLORD1:40;
then consider f being Function such that
A5: f is_isomorphism_of RelIncl (order_type_of (R |_2 X)),R |_2 X ;
field (RelIncl (order_type_of (R |_2 X))) = order_type_of (R |_2 X) by WELLORD2:def 1;
then A6: dom f = order_type_of (R |_2 X) by A5;
A7: rng f = X by A4, A5;
defpred S₂[ object ] means for A, B being Ordinal st B in A & $1 = A holds
f . B c= f . A;
consider Y being set such that
A8: for x being set holds
( x in Y iff ( x in dom f & S₂[x] ) ) from XFAMILY:sch 1();
take Z = f .: Y; :: thesis: ( Z c= X & union Z = union X & ( for Z being set st Z c= Z & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )
thus Z c= X by A7, RELAT_1:111; :: thesis: ( union Z = union X & ( for Z being set st Z c= Z & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )
thus union Z c= union X by A7, RELAT_1:111, ZFMISC_1:77; :: according to XBOOLE_0:def 10 :: thesis: ( union X c= union Z & ( for Z being set st Z c= Z & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )
thus union X c= union Z :: thesis: for Z being set st Z c= Z & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) )

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union X or x in union Z )
assume x in union X ; :: thesis: x in union Z
then consider Z1 being set such that
A9: x in Z1 and
A10: Z1 in X by TARSKI:def 4;
consider y being object such that
A11: y in dom f and
A12: Z1 = f . y by A7, A10, FUNCT_1:def 3;
reconsider y = y as Ordinal by A6, A11;
defpred S₃[ Ordinal] means ( $1 c= y & x in f . $1 );
A13: ex A being Ordinal st S₃[A] by A9, A12;
consider A being Ordinal such that
A14: ( S₃[A] & ( for B being Ordinal st S₃[B] holds
A c= B ) ) from ORDINAL1:sch 1(A13);
A15: A in dom f by A6, A11, A14, ORDINAL1:12;

now :: thesis: for B, C being Ordinal st C in B & A = B holds
f . C c= f . B

let B, C be Ordinal; :: thesis: ( C in B & A = B implies f . C c= f . B )
assume that
A16: C in B and
A17: A = B ; :: thesis: f . C c= f . B
A18: C in dom f by A6, A11, A14, A16, A17, ORDINAL1:10;
A19: ( not C c= y or not x in f . C ) by A14, A16, A17, ORDINAL1:5;
A20: f . A in X by A7, A15, FUNCT_1:def 3;
f . C in X by A7, A18, FUNCT_1:def 3;
then f . C,f . A are_c=-comparable by A1, A20;
then ( f . C c= f . A or f . A c= f . C ) ;
hence f . C c= f . B by A14, A16, A17, A19, ORDINAL1:def 2; :: thesis: verum

end;

then A in Y by A8, A15;
then f . A in Z by A15, FUNCT_1:def 6;
hence x in union Z by A14, TARSKI:def 4; :: thesis: verum

end;

let V be set ; :: thesis: ( V c= Z & V <> {} implies ex Z1 being set st
( Z1 in V & ( for Z2 being set st Z2 in V holds
Z1 c= Z2 ) ) )
assume that
A21: V c= Z and
A22: V <> {} ; :: thesis: ex Z1 being set st
( Z1 in V & ( for Z2 being set st Z2 in V holds
Z1 c= Z2 ) )
set x = the Element of V;
the Element of V in Z by A21, A22;
then consider y being object such that
A23: y in dom f and
A24: y in Y and
A25: the Element of V = f . y by FUNCT_1:def 6;
reconsider y = y as Ordinal by A6, A23;
defpred S₃[ Ordinal] means ( $1 in Y & f . $1 in V );
y = y ;
then A26: ex A being Ordinal st S₃[A] by A22, A24, A25;
consider A being Ordinal such that
A27: ( S₃[A] & ( for B being Ordinal st S₃[B] holds
A c= B ) ) from ORDINAL1:sch 1(A26);
take Z1 = f . A; :: thesis: ( Z1 in V & ( for Z2 being set st Z2 in V holds
Z1 c= Z2 ) )
thus Z1 in V by A27; :: thesis: for Z2 being set st Z2 in V holds
Z1 c= Z2
let Z2 be set ; :: thesis: ( Z2 in V implies Z1 c= Z2 )
assume A28: Z2 in V ; :: thesis: Z1 c= Z2
then consider y being object such that
A29: y in dom f and
A30: y in Y and
A31: Z2 = f . y by A21, FUNCT_1:def 6;
reconsider y = y as Ordinal by A6, A29;
( A c< y iff ( A c= y & A <> y ) ) ;
then ( A = y or A in y ) by A27, A28, A30, A31, ORDINAL1:11;
hence Z1 c= Z2 by A8, A30, A31; :: thesis: verum