let X be set ; :: thesis:
let Y be Subset-Family of X; :: thesis:
assume that
A1: ( Y is finite & not Y is with_empty_element & Y is c=-linear ) and
A2: X in Y ; :: thesis:
defpred S₁[ set , set ] means ( $1 in $2 & $2 in Y & ( for y being set st y in Y & $1 in y holds
$2 c= y ) );
A3: for x being set st x in X holds
ex y being set st S₁[x,y]

let x be set ; :: thesis:
set U = { A where A is Subset of X : ( x in A & A in Y ) } ;
A4: { A where A is Subset of X : ( x in A & A in Y ) } c= Y

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in { A where A is Subset of X : ( x in A & A in Y ) } ; :: thesis:
then ex A being Subset of X st
( y = A & x in A & A in Y ) ;
hence y in Y ; :: thesis:

end;

then reconsider U = { A where A is Subset of X : ( x in A & A in Y ) } as Subset-Family of X by XBOOLE_1:1;
assume x in X ; :: thesis:
then X in U by A2;
then consider m being set such that
A5: m in U and
A6: for y being set st y in U holds
m c= y by A1, A4, FINSET_1:30;
take m ; :: thesis:
ex A being Subset of X st
( m = A & x in A & A in Y ) by A5;
hence ( x in m & m in Y ) ; :: thesis:
let y be set ; :: thesis:
assume ( y in Y & x in y ) ; :: thesis:
then y in U ;
hence m c= y by A6; :: thesis:

end;

consider f being Function such that
A7: ( dom f = X & ( for x being set st x in X holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A3);
defpred S₂[ set , set ] means ( ( $2 in Y or $2 is empty ) & $2 c< $1 & ( for x being set st x in Y & x c< $1 holds
x c= $2 ) & ( for x being set st x in Y & $2 c= x & x c= $1 & not x = $1 holds
x = $2 ) );
A8: for x being set st x in Y holds
ex y being set st
( y in bool X & S₂[x,y] )

proof

let x be set ; :: thesis:
assume A9: x in Y ; :: thesis:
set U = { A where A is Subset of X : ( A c< x & A in Y ) } ;
A10: { A where A is Subset of X : ( A c< x & A in Y ) } c= Y

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in { A where A is Subset of X : ( A c< x & A in Y ) } ; :: thesis:
then ex A being Subset of X st
( y = A & A c< x & A in Y ) ;
hence y in Y ; :: thesis:

end;

then reconsider U = { A where A is Subset of X : ( A c< x & A in Y ) } as Subset-Family of X by XBOOLE_1:1;
take u = union U; :: thesis:
thus u in bool X ; :: thesis:
A11: for y being set st y in Y & y c< x holds
y c= u

proof

let y be set ; :: thesis:
assume that
A12: y in Y and
A13: y c< x ; :: thesis:
reconsider A = y as Subset of X by A12;
y in U by A12, A13;
hence y c= u by ZFMISC_1:92; :: thesis:

end;

per cases ;

suppose U is empty ; :: thesis:

hence ( ( u in Y or u is empty ) & u c< x & ( for y being set st y in Y & y c< x holds
y c= u ) ) by A1, A9, A11, XBOOLE_1:61, ZFMISC_1:2; :: thesis:
let y be set ; :: thesis:
assume that
A14: y in Y and
A15: u c= y and
A16: y c= x ; :: thesis:
assume y <> x ; :: thesis:
then y c< x by A16, XBOOLE_0:def 8;
then y c= u by A11, A14;
hence y = u by A15, XBOOLE_0:def 10; :: thesis:

end;

suppose not U is empty ; :: thesis:

then u in U by A1, A10, Th9;
then ex A being Subset of X st
( A = u & A c< x & A in Y ) ;
hence ( ( u in Y or u is empty ) & u c< x & ( for y being set st y in Y & y c< x holds
y c= u ) ) by A11; :: thesis:
let y be set ; :: thesis:
assume that
A17: y in Y and
A18: u c= y and
A19: y c= x ; :: thesis:
assume y <> x ; :: thesis:
then y c< x by A19, XBOOLE_0:def 8;
then y c= u by A11, A17;
hence y = u by A18, XBOOLE_0:def 10; :: thesis:

end;

consider g being Function of Y,(bool X) such that
A20: for x being set st x in Y holds
S₂[x,g . x] from FUNCT_2:sch 1(A8);
defpred S₃[ set , set ] means ex h being Function of ($1 \ (g . $1)),(bool ($1 \ (g . $1))) st
( $2 = h & h is one-to-one & not rng h is with_empty_element & rng h is c=-linear & dom h in rng h & ( for Z being set st Z in rng h & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng h ) ) );
A21: for x being set st x in Y holds
ex y being set st S₃[x,y]

proof

let y be set ; :: thesis:
assume y in Y ; :: thesis:
then g . y c< y by A20;
then y \ (g . y) <> {} by XBOOLE_1:105;
then consider Z being Subset-Family of (y \ (g . y)) such that
A22: ( not Z is with_empty_element & Z is c=-linear & y \ (g . y) in Z ) and
A23: card (y \ (g . y)) = card Z and
A24: for z being set st z in Z & card z <> 1 holds
ex x being set st
( x in z & z \ {x} in Z ) by Th12;
y \ (g . y),Z are_equipotent by A23, CARD_1:21;
then consider h being Function such that
A25: h is one-to-one and
A26: ( dom h = y \ (g . y) & rng h = Z ) by WELLORD2:def 4;
reconsider h = h as Function of (y \ (g . y)),(bool (y \ (g . y))) by A26, FUNCT_2:4;
take h ; :: thesis:
thus S₃[y,h] by A22, A24, A25, A26; :: thesis:

end;

consider h being Function such that
A27: ( dom h = Y & ( for x being set st x in Y holds
S₃[x,h . x] ) ) from CLASSES1:sch 1(A21);

now

let x be set ; :: thesis:
assume x in dom h ; :: thesis:
then ex H being Function of (x \ (g . x)),(bool (x \ (g . x))) st
( h . x = H & H is one-to-one & not rng H is with_empty_element & rng H is c=-linear & dom H in rng H & ( for Z being set st Z in rng H & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H ) ) ) by A27;
hence h . x is Function ; :: thesis:

end;

then reconsider h = h as Function-yielding Function by FUNCOP_1:def 6;
deffunc H₁( set ) -> set = (g . (f . $1)) \/ ((h . (f . $1)) . $1);
A28: for x being set st x in X holds
x in (f . x) \ (g . (f . x))

proof

let x be set ; :: thesis:
assume A29: x in X ; :: thesis:
then A30: f . x in Y by A7;
assume A31: not x in (f . x) \ (g . (f . x)) ; :: thesis:
x in f . x by A7, A29;
then A32: x in g . (f . x) by A31, XBOOLE_0:def 5;
then g . (f . x) in Y by A20, A30;
then A33: f . x c= g . (f . x) by A7, A32;
g . (f . x) c< f . x by A20, A30;
hence contradiction by A33, XBOOLE_0:def 8; :: thesis:

end;

A34: for x being set st x in X holds
H₁(x) in bool X

proof

let x be set ; :: thesis:
set fx = f . x;
assume A35: x in X ; :: thesis:
then A36: f . x in Y by A7;
then consider H being Function of ((f . x) \ (g . (f . x))),(bool ((f . x) \ (g . (f . x)))) such that
A37: h . (f . x) = H and
H is one-to-one and
( not rng H is with_empty_element & rng H is c=-linear ) and
dom H in rng H and
for Z being set st Z in rng H & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H ) by A27;
A38: x in (f . x) \ (g . (f . x)) by A28, A35;
dom H = (f . x) \ (g . (f . x)) by FUNCT_2:def 1;
then H . x in rng H by A38, FUNCT_1:def 5;
then H . x c= f . x by XBOOLE_1:1;
then A39: H . x c= X by A36, XBOOLE_1:1;
( g . (f . x) in Y or g . (f . x) is empty ) by A20, A36;
then H₁(x) c= X by A37, A39, XBOOLE_1:8;
hence H₁(x) in bool X ; :: thesis:

end;

consider z being Function of X,(bool X) such that
A40: for x being set st x in X holds
z . x = H₁(x) from FUNCT_2:sch 2(A34);
A41: dom z = X by FUNCT_2:def 1;
A42: Y c= rng z

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume A43: y in Y ; :: thesis:
then consider H being Function of (y \ (g . y)),(bool (y \ (g . y))) such that
A44: h . y = H and
H is one-to-one and
( not rng H is with_empty_element & rng H is c=-linear ) and
A45: dom H in rng H and
for Z being set st Z in rng H & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H ) by A27;
consider x being set such that
A46: x in dom H and
A47: H . x = dom H by A45, FUNCT_1:def 5;
A48: dom H = y \ (g . y) by FUNCT_2:def 1;
then A49: x in y by A46;
then A50: x in f . x by A7, A43;
g . y c< y by A20, A43;
then A51: g . y c= y by XBOOLE_0:def 8;
A52: f . x c= y by A7, A43, A49;
A53: f . x in Y by A7, A43, A49;
f . x = y

proof

assume f . x <> y ; :: thesis:
then f . x c< y by A52, XBOOLE_0:def 8;
then f . x c= g . y by A20, A43, A53;
hence contradiction by A46, A50, XBOOLE_0:def 5; :: thesis:

end;

then z . x = (g . y) \/ (y \ (g . y)) by A40, A43, A44, A47, A48, A49
.= y by A51, XBOOLE_1:45 ;
hence y in rng z by A41, A43, A49, FUNCT_1:def 5; :: thesis:

end;

A54: for Z being set st Z in rng z & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng z )

proof

let Z be set ; :: thesis:
assume that
A55: Z in rng z and
A56: card Z <> 1 ; :: thesis:
consider x being set such that
A57: x in dom z and
A58: z . x = Z by A55, FUNCT_1:def 5;
set fx = f . x;
A59: f . x in Y by A7, A57;
then consider H being Function of ((f . x) \ (g . (f . x))),(bool ((f . x) \ (g . (f . x)))) such that
A60: h . (f . x) = H and
H is one-to-one and
( not rng H is with_empty_element & rng H is c=-linear ) and
dom H in rng H and
A61: for Z being set st Z in rng H & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H ) by A27;
A62: z . x = (g . (f . x)) \/ (H . x) by A40, A57, A60;
A63: dom H = (f . x) \ (g . (f . x)) by FUNCT_2:def 1;
x in (f . x) \ (g . (f . x)) by A28, A57;
then A64: H . x in rng H by A63, FUNCT_1:def 5;

per cases ;

suppose A65: card (H . x) = 1 ; :: thesis:

then g . (f . x) <> {} by A56, A58, A62;
then A66: g . (f . x) in Y by A20, A59;
consider a being set such that
A67: H . x = {a} by A65, CARD_2:60;
take a ; :: thesis:
A68: a in H . x by A67, TARSKI:def 1;
then A69: not a in g . (f . x) by A64, XBOOLE_0:def 5;
thus a in Z by A58, A62, A68, XBOOLE_0:def 3; :: thesis:
Z \ {a} = ((g . (f . x)) \/ (H . x)) \ (H . x) by A40, A57, A58, A60, A67
.= (g . (f . x)) \ (H . x) by XBOOLE_1:40
.= g . (f . x) by A67, A69, ZFMISC_1:65 ;
hence Z \ {a} in rng z by A42, A66; :: thesis:

end;

suppose card (H . x) <> 1 ; :: thesis:

then consider a being set such that
A70: a in H . x and
A71: (H . x) \ {a} in rng H by A61, A64;
A72: not a in g . (f . x) by A64, A70, XBOOLE_0:def 5;
take a ; :: thesis:
thus a in Z by A58, A62, A70, XBOOLE_0:def 3; :: thesis:
consider b being set such that
A73: b in dom H and
A74: H . b = (H . x) \ {a} by A71, FUNCT_1:def 5;
A75: b in f . x by A63, A73;
then A76: b in f . b by A7, A59;
A77: f . b in Y by A7, A59, A75;
A78: f . b c= f . x by A7, A59, A75;
f . x = f . b

proof

assume f . x <> f . b ; :: thesis:
then f . b c< f . x by A78, XBOOLE_0:def 8;
then f . b c= g . (f . x) by A20, A59, A77;
hence contradiction by A73, A76, XBOOLE_0:def 5; :: thesis:

end;

then z . b = (g . (f . x)) \/ ((H . x) \ {a}) by A40, A59, A60, A74, A75
.= ((g . (f . x)) \/ (H . x)) \ {a} by A72, XBOOLE_1:87, ZFMISC_1:56
.= Z \ {a} by A58, A40, A57, A60 ;
hence Z \ {a} in rng z by A41, A59, A75, FUNCT_1:def 5; :: thesis:

end;

A79: rng z is c=-linear

proof

let y1, y2 be set ; :: according to ORDINAL1:def 9 :: thesis:
assume that
A80: y1 in rng z and
A81: y2 in rng z ; :: thesis:
consider x1 being set such that
A82: x1 in dom z and
A83: z . x1 = y1 by A80, FUNCT_1:def 5;
consider x2 being set such that
A84: x2 in dom z and
A85: z . x2 = y2 by A81, FUNCT_1:def 5;
set fx1 = f . x1;
set fx2 = f . x2;
A86: x1 in (f . x1) \ (g . (f . x1)) by A28, A82;
A87: f . x1 in Y by A7, A82;
then consider H1 being Function of ((f . x1) \ (g . (f . x1))),(bool ((f . x1) \ (g . (f . x1)))) such that
A88: h . (f . x1) = H1 and
H1 is one-to-one and
( not rng H1 is with_empty_element & rng H1 is c=-linear ) and
dom H1 in rng H1 and
for Z being set st Z in rng H1 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H1 ) by A27;
A89: z . x1 = (g . (f . x1)) \/ (H1 . x1) by A40, A82, A88;
dom H1 = (f . x1) \ (g . (f . x1)) by FUNCT_2:def 1;
then A90: H1 . x1 in rng H1 by A86, FUNCT_1:def 5;
A91: x2 in (f . x2) \ (g . (f . x2)) by A28, A84;
A92: f . x2 in Y by A7, A84;
then consider H2 being Function of ((f . x2) \ (g . (f . x2))),(bool ((f . x2) \ (g . (f . x2)))) such that
A93: h . (f . x2) = H2 and
H2 is one-to-one and
A94: ( not rng H2 is with_empty_element & rng H2 is c=-linear ) and
dom H2 in rng H2 and
for Z being set st Z in rng H2 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H2 ) by A27;
A95: z . x2 = (g . (f . x2)) \/ (H2 . x2) by A40, A84, A93;
dom H2 = (f . x2) \ (g . (f . x2)) by FUNCT_2:def 1;
then A96: H2 . x2 in rng H2 by A91, FUNCT_1:def 5;
A97: f . x1,f . x2 are_c=-comparable by A1, A87, A92, ORDINAL1:def 9;

per cases by A97, XBOOLE_0:def 9;

suppose A98: f . x1 = f . x2 ; :: thesis:

then H1 . x1,H1 . x2 are_c=-comparable by A88, A90, A93, A94, A96, ORDINAL1:def 9;
then ( H1 . x1 c= H1 . x2 or H1 . x2 c= H1 . x1 ) by XBOOLE_0:def 9;
then ( z . x1 c= z . x2 or z . x2 c= z . x1 ) by A88, A89, A93, A95, A98, XBOOLE_1:9;
hence y1,y2 are_c=-comparable by A83, A85, XBOOLE_0:def 9; :: thesis:

end;

suppose ( f . x1 c= f . x2 & f . x1 <> f . x2 ) ; :: thesis:

then f . x1 c< f . x2 by XBOOLE_0:def 8;
then A99: f . x1 c= g . (f . x2) by A20, A87, A92;
g . (f . x2) c= z . x2 by A95, XBOOLE_1:7;
then A100: f . x1 c= z . x2 by A99, XBOOLE_1:1;
g . (f . x1) c< f . x1 by A20, A87;
then g . (f . x1) c= f . x1 by XBOOLE_0:def 8;
then A101: (g . (f . x1)) \/ ((f . x1) \ (g . (f . x1))) = f . x1 by XBOOLE_1:45;
z . x1 c= (g . (f . x1)) \/ ((f . x1) \ (g . (f . x1))) by A89, A90, XBOOLE_1:9;
then z . x1 c= z . x2 by A100, A101, XBOOLE_1:1;
hence y1,y2 are_c=-comparable by A83, A85, XBOOLE_0:def 9; :: thesis:

end;

suppose ( f . x2 c= f . x1 & f . x1 <> f . x2 ) ; :: thesis:

then f . x2 c< f . x1 by XBOOLE_0:def 8;
then A102: f . x2 c= g . (f . x1) by A20, A87, A92;
g . (f . x1) c= z . x1 by A89, XBOOLE_1:7;
then A103: f . x2 c= z . x1 by A102, XBOOLE_1:1;
g . (f . x2) c< f . x2 by A20, A92;
then g . (f . x2) c= f . x2 by XBOOLE_0:def 8;
then A104: (g . (f . x2)) \/ ((f . x2) \ (g . (f . x2))) = f . x2 by XBOOLE_1:45;
z . x2 c= (g . (f . x2)) \/ ((f . x2) \ (g . (f . x2))) by A95, A96, XBOOLE_1:9;
then z . x2 c= z . x1 by A103, A104, XBOOLE_1:1;
hence y1,y2 are_c=-comparable by A83, A85, XBOOLE_0:def 9; :: thesis:

end;

A105: not rng z is with_empty_element

proof

assume rng z is with_empty_element ; :: thesis:
then {} in rng z by SETFAM_1:def 9;
then consider x being set such that
A106: x in dom z and
A107: z . x = {} by FUNCT_1:def 5;
set fx = f . x;
A108: x in (f . x) \ (g . (f . x)) by A28, A106;
f . x in Y by A7, A106;
then consider H being Function of ((f . x) \ (g . (f . x))),(bool ((f . x) \ (g . (f . x)))) such that
A109: h . (f . x) = H and
H is one-to-one and
A110: ( not rng H is with_empty_element & rng H is c=-linear ) and
dom H in rng H and
for Z being set st Z in rng H & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H ) by A27;
dom H = (f . x) \ (g . (f . x)) by FUNCT_2:def 1;
then A111: H . x in rng H by A108, FUNCT_1:def 5;
z . x = (g . (f . x)) \/ (H . x) by A40, A106, A109;
hence contradiction by A107, A110, A111; :: thesis:

end;

take rng z ; :: thesis:
for x1, x2 being set st x1 in dom z & x2 in dom z & z . x1 = z . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis:
set f1 = f . x1;
set f2 = f . x2;
assume that
A112: x1 in dom z and
A113: x2 in dom z and
A114: z . x1 = z . x2 ; :: thesis:
A115: ( z . x1 = H₁(x1) & z . x2 = H₁(x2) ) by A40, A112, A113;
A116: f . x2 in Y by A7, A113;
then consider H2 being Function of ((f . x2) \ (g . (f . x2))),(bool ((f . x2) \ (g . (f . x2)))) such that
A117: h . (f . x2) = H2 and
A118: H2 is one-to-one and
A119: ( not rng H2 is with_empty_element & rng H2 is c=-linear ) and
dom H2 in rng H2 and
for Z being set st Z in rng H2 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H2 ) by A27;
dom H2 = (f . x2) \ (g . (f . x2)) by FUNCT_2:def 1;
then A120: x2 in dom H2 by A28, A113;
then A121: H2 . x2 in rng H2 by FUNCT_1:def 5;
then A122: g . (f . x2) misses H2 . x2 by XBOOLE_1:63, XBOOLE_1:79;
A123: f . x1 in Y by A7, A112;
then consider H1 being Function of ((f . x1) \ (g . (f . x1))),(bool ((f . x1) \ (g . (f . x1)))) such that
A124: h . (f . x1) = H1 and
H1 is one-to-one and
A125: ( not rng H1 is with_empty_element & rng H1 is c=-linear ) and
dom H1 in rng H1 and
for Z being set st Z in rng H1 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H1 ) by A27;
dom H1 = (f . x1) \ (g . (f . x1)) by FUNCT_2:def 1;
then A126: x1 in dom H1 by A28, A112;
then A127: H1 . x1 in rng H1 by FUNCT_1:def 5;
then A128: g . (f . x1) misses H1 . x1 by XBOOLE_1:63, XBOOLE_1:79;
A129: f . x1,f . x2 are_c=-comparable by A1, A116, A123, ORDINAL1:def 9;

per cases by A129, XBOOLE_0:def 9;

suppose A130: f . x1 = f . x2 ; :: thesis:

then H1 . x1 = H1 . x2 by A114, A115, A117, A122, A124, A128, XBOOLE_1:71;
hence x1 = x2 by A117, A118, A120, A124, A126, A130, FUNCT_1:def 8; :: thesis:

end;

suppose A131: ( f . x1 c= f . x2 & f . x1 <> f . x2 ) ; :: thesis:

g . (f . x1) c< f . x1 by A20, A123;
then g . (f . x1) c= f . x1 by XBOOLE_0:def 8;
then (g . (f . x1)) \/ ((f . x1) \ (g . (f . x1))) = f . x1 by XBOOLE_1:45;
then A132: H₁(x2) c= f . x1 by A114, A115, A124, A127, XBOOLE_1:9;
f . x1 c< f . x2 by A131, XBOOLE_0:def 8;
then f . x1 c= g . (f . x2) by A20, A116, A123;
then H₁(x2) c= g . (f . x2) by A132, XBOOLE_1:1;
then H2 . x2 c= g . (f . x2) by A117, XBOOLE_1:11;
hence x1 = x2 by A119, A121, XBOOLE_1:67, XBOOLE_1:79; :: thesis:

end;

suppose A133: ( f . x2 c= f . x1 & f . x1 <> f . x2 ) ; :: thesis:

g . (f . x2) c< f . x2 by A20, A116;
then g . (f . x2) c= f . x2 by XBOOLE_0:def 8;
then (g . (f . x2)) \/ ((f . x2) \ (g . (f . x2))) = f . x2 by XBOOLE_1:45;
then A134: H₁(x1) c= f . x2 by A114, A115, A117, A121, XBOOLE_1:9;
f . x2 c< f . x1 by A133, XBOOLE_0:def 8;
then f . x2 c= g . (f . x1) by A20, A116, A123;
then H₁(x1) c= g . (f . x1) by A134, XBOOLE_1:1;
then H1 . x1 c= g . (f . x1) by A124, XBOOLE_1:11;
hence x1 = x2 by A125, A127, XBOOLE_1:67, XBOOLE_1:79; :: thesis:

end;

then z is one-to-one by FUNCT_1:def 8;
then X, rng z are_equipotent by A41, WELLORD2:def 4;
hence ( Y c= rng z & not rng z is with_empty_element & rng z is c=-linear & card X = card (rng z) & ( for Z being set st Z in rng z & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng z ) ) ) by A42, A54, A79, A105, CARD_1:21; :: thesis: