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

let x be object ; :: 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 object ; :: 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:11;
take m ; :: thesis:
consider A being Subset of X such that
A7: ( m = A & x in A & A in Y ) by A5;
take A ; :: thesis:
thus A = m by A7; :: thesis:
thus ( x in A & m in Y ) by A7; :: thesis:
let y be set ; :: thesis:
assume ( y in Y & x in y ) ; :: thesis:
then y in U ;
hence A c= y by A6, A7; :: thesis:

end;

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

proof

let x be object ; :: thesis:
reconsider xx = x as set by TARSKI:1;
assume A10: x in Y ; :: thesis:
set U = { A where A is Subset of X : ( A c< xx & A in Y ) } ;
A11: { A where A is Subset of X : ( A c< xx & A in Y ) } c= Y

proof

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

end;

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

proof

let y be set ; :: thesis:
assume that
A13: y in Y and
A14: y c< xx ; :: thesis:
y in U by A13, A14;
hence y c= u by ZFMISC_1:74; :: thesis:

end;

per cases ;

suppose A15: U is empty ; :: thesis:

take xx ; :: thesis:
take u ; :: thesis:
thus ( xx = x & u = u ) ; :: thesis:
thus ( ( u in Y or u is empty ) & u c< xx & ( for y being set st y in Y & y c< xx holds
y c= u ) ) by A1, A10, A12, A15, XBOOLE_1:61, ZFMISC_1:2; :: thesis:
let y be set ; :: thesis:
assume that
A16: y in Y and
A17: u c= y and
A18: y c= xx ; :: thesis:
assume y <> xx ; :: thesis:
then y c< xx by A18;
then y c= u by A12, A16;
hence y = u by A17; :: thesis:

end;

suppose not U is empty ; :: thesis:

then u in U by A1, A11, Th9;
then A19: ex A being Subset of X st
( A = u & A c< xx & A in Y ) ;
take xx ; :: thesis:
take u ; :: thesis:
thus ( xx = x & u = u ) ; :: thesis:
thus ( ( u in Y or u is empty ) & u c< xx & ( for y being set st y in Y & y c< xx holds
y c= u ) ) by A12, A19; :: thesis:
let y be set ; :: thesis:
assume that
A20: y in Y and
A21: u c= y and
A22: y c= xx ; :: thesis:
assume y <> xx ; :: thesis:
then y c< xx by A22;
then y c= u by A12, A20;
hence y = u by A21; :: thesis:

end;

consider g being Function of Y,(bool X) such that
A23: for x being object st x in Y holds
S₂[x,g . x] from FUNCT_2:sch 1(A9);
defpred S₃[ object , object ] means ex A being set ex h being Function of (A \ (g . A)),(bool (A \ (g . A))) st
( A = $1 & $2 = h & h is one-to-one & rng h is with_non-empty_elements & 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 ) ) );
A24: for x being object st x in Y holds
ex y being object st S₃[x,y]

proof

let y be object ; :: thesis:
assume A25: y in Y ; :: thesis:
reconsider y = y as set by TARSKI:1;
S₂[y,g . y] by A23, A25;
then g . y c< y ;
then y \ (g . y) <> {} by XBOOLE_1:105;
then consider Z being Subset-Family of (y \ (g . y)) such that
A26: ( Z is with_non-empty_elements & Z is c=-linear & y \ (g . y) in Z ) and
A27: card (y \ (g . y)) = card Z and
A28: 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 A27, CARD_1:5;
then consider h being Function such that
A29: h is one-to-one and
A30: ( 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 A30, FUNCT_2:2;
take h ; :: thesis:
thus S₃[y,h] by A26, A28, A29, A30; :: thesis:

end;

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

now :: thesis:

let x be object ; :: thesis:
assume x in dom h ; :: thesis:
then S₃[x,h . x] by A31;
hence h . x is Function ; :: thesis:

end;

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

proof

let x be set ; :: thesis:
assume x in X ; :: thesis:
then A33: S₁[x,f . x] by A8;
then A34: f . x in Y ;
assume A35: not x in (f . x) \ (g . (f . x)) ; :: thesis:
x in f . x by A33;
then A36: x in g . (f . x) by A35, XBOOLE_0:def 5;
A37: S₂[f . x,g . (f . x)] by A23, A34;
then g . (f . x) in Y by A36;
then A38: f . x c= g . (f . x) by A36, A33;
g . (f . x) c< f . x by A37;
hence contradiction by A38, XBOOLE_0:def 8; :: thesis:

end;

A39: for x being object st x in X holds
H₁(x) in bool X

proof

let x be object ; :: thesis:
set fx = f . x;
assume A40: x in X ; :: thesis:
then S₁[x,f . x] by A8;
then A41: f . x in Y ;
then S₃[f . x,h . (f . x)] by A31;
then consider A being set , H being Function of ((f . x) \ (g . (f . x))),(bool ((f . x) \ (g . (f . x)))) such that
A42: h . (f . x) = H and
H is one-to-one and
( rng H is with_non-empty_elements & 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 ) ;
A43: x in (f . x) \ (g . (f . x)) by A32, A40;
dom H = (f . x) \ (g . (f . x)) by FUNCT_2:def 1;
then H . x in rng H by A43, FUNCT_1:def 3;
then H . x c= f . x by XBOOLE_1:1;
then A44: H . x c= X by A41, XBOOLE_1:1;
S₂[f . x,g . (f . x)] by A23, A41;
then ( g . (f . x) in Y or g . (f . x) is empty ) ;
then H₁(x) c= X by A42, A44, XBOOLE_1:8;
hence H₁(x) in bool X ; :: thesis:

end;

consider z being Function of X,(bool X) such that
A45: for x being object st x in X holds
z . x = H₁(x) from FUNCT_2:sch 2(A39);
A46: dom z = X by FUNCT_2:def 1;
A47: Y c= rng z

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
reconsider yy = y as set by TARSKI:1;
assume A48: y in Y ; :: thesis:
then S₃[y,h . y] by A31;
then consider H being Function of (yy \ (g . y)),(bool (yy \ (g . y))) such that
A49: h . y = H and
H is one-to-one and
( rng H is with_non-empty_elements & rng H is c=-linear ) and
A50: 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 ) ;
consider x being object such that
A51: x in dom H and
A52: H . x = dom H by A50, FUNCT_1:def 3;
A53: dom H = yy \ (g . yy) by FUNCT_2:def 1;
then A54: x in yy by A51;
then A55: S₁[x,f . x] by A8, A48;
then A56: x in f . x ;
S₂[y,g . y] by A23, A48;
then g . y c< yy ;
then A57: g . y c= yy ;
A58: f . x c= yy by A48, A54, A55;
A59: f . x in Y by A55;
f . x = y

proof

assume f . x <> y ; :: thesis:
then A60: f . x c< yy by A58;
S₂[y,g . y] by A23, A48;
then f . x c= g . y by A59, A60;
hence contradiction by A51, A56, XBOOLE_0:def 5; :: thesis:

end;

then z . x = (g . y) \/ (yy \ (g . y)) by A45, A48, A49, A52, A53, A54
.= y by A57, XBOOLE_1:45 ;
hence y in rng z by A46, A48, A54, FUNCT_1:def 3; :: thesis:

end;

A61: 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
A62: Z in rng z and
A63: card Z <> 1 ; :: thesis:
consider x being object such that
A64: x in dom z and
A65: z . x = Z by A62, FUNCT_1:def 3;
set fx = f . x;
S₁[x,f . x] by A8, A64;
then A66: f . x in Y ;
then S₃[f . x,h . (f . x)] by A31;
then consider H being Function of ((f . x) \ (g . (f . x))),(bool ((f . x) \ (g . (f . x)))) such that
A67: h . (f . x) = H and
H is one-to-one and
( rng H is with_non-empty_elements & rng H is c=-linear ) and
dom H in rng H and
A68: 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 ) ;
A69: z . x = (g . (f . x)) \/ (H . x) by A45, A64, A67;
A70: dom H = (f . x) \ (g . (f . x)) by FUNCT_2:def 1;
x in (f . x) \ (g . (f . x)) by A32, A64;
then A71: H . x in rng H by A70, FUNCT_1:def 3;

per cases ;

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

then A73: g . (f . x) <> {} by A63, A65, A69;
S₂[f . x,g . (f . x)] by A23, A66;
then A74: g . (f . x) in Y by A73;
consider a being object such that
A75: H . x = {a} by A72, CARD_2:42;
reconsider a = a as set by TARSKI:1;
take a ; :: thesis:
A76: a in H . x by A75, TARSKI:def 1;
then A77: not a in g . (f . x) by A71, XBOOLE_0:def 5;
thus a in Z by A65, A69, A76, XBOOLE_0:def 3; :: thesis:
Z \ {a} = ((g . (f . x)) \/ (H . x)) \ (H . x) by A45, A64, A65, A67, A75
.= (g . (f . x)) \ (H . x) by XBOOLE_1:40
.= g . (f . x) by A75, A77, ZFMISC_1:57 ;
hence Z \ {a} in rng z by A47, A74; :: thesis:

end;

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

then consider a being set such that
A78: a in H . x and
A79: (H . x) \ {a} in rng H by A68, A71;
A80: not a in g . (f . x) by A71, A78, XBOOLE_0:def 5;
take a ; :: thesis:
thus a in Z by A65, A69, A78, XBOOLE_0:def 3; :: thesis:
consider b being object such that
A81: b in dom H and
A82: H . b = (H . x) \ {a} by A79, FUNCT_1:def 3;
A83: b in f . x by A70, A81;
then A84: S₁[b,f . b] by A8, A66;
then A85: b in f . b ;
A86: f . b in Y by A84;
A87: f . b c= f . x by A66, A83, A84;
f . x = f . b

proof

assume f . x <> f . b ; :: thesis:
then A88: f . b c< f . x by A87;
S₂[f . x,g . (f . x)] by A23, A66;
then f . b c= g . (f . x) by A86, A88;
hence contradiction by A81, A85, XBOOLE_0:def 5; :: thesis:

end;

then z . b = (g . (f . x)) \/ ((H . x) \ {a}) by A45, A66, A67, A82, A83
.= ((g . (f . x)) \/ (H . x)) \ {a} by A80, XBOOLE_1:87, ZFMISC_1:50
.= Z \ {a} by A65, A45, A64, A67 ;
hence Z \ {a} in rng z by A46, A66, A83, FUNCT_1:def 3; :: thesis:

end;

A89: rng z is c=-linear

proof

let y1, y2 be set ; :: according to ORDINAL1:def 8 :: thesis:
assume that
A90: y1 in rng z and
A91: y2 in rng z ; :: thesis:
consider x1 being object such that
A92: x1 in dom z and
A93: z . x1 = y1 by A90, FUNCT_1:def 3;
consider x2 being object such that
A94: x2 in dom z and
A95: z . x2 = y2 by A91, FUNCT_1:def 3;
set fx1 = f . x1;
set fx2 = f . x2;
A96: x1 in (f . x1) \ (g . (f . x1)) by A32, A92;
S₁[x1,f . x1] by A8, A92;
then A97: f . x1 in Y ;
then S₃[f . x1,h . (f . x1)] by A31;
then consider H1 being Function of ((f . x1) \ (g . (f . x1))),(bool ((f . x1) \ (g . (f . x1)))) such that
A98: h . (f . x1) = H1 and
H1 is one-to-one and
( rng H1 is with_non-empty_elements & 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 ) ;
A99: z . x1 = (g . (f . x1)) \/ (H1 . x1) by A45, A92, A98;
dom H1 = (f . x1) \ (g . (f . x1)) by FUNCT_2:def 1;
then A100: H1 . x1 in rng H1 by A96, FUNCT_1:def 3;
A101: x2 in (f . x2) \ (g . (f . x2)) by A32, A94;
S₁[x2,f . x2] by A8, A94;
then A102: f . x2 in Y ;
then S₃[f . x2,h . (f . x2)] by A31;
then consider H2 being Function of ((f . x2) \ (g . (f . x2))),(bool ((f . x2) \ (g . (f . x2)))) such that
A103: h . (f . x2) = H2 and
H2 is one-to-one and
A104: ( rng H2 is with_non-empty_elements & 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 ) ;
A105: z . x2 = (g . (f . x2)) \/ (H2 . x2) by A45, A94, A103;
dom H2 = (f . x2) \ (g . (f . x2)) by FUNCT_2:def 1;
then A106: H2 . x2 in rng H2 by A101, FUNCT_1:def 3;
A107: f . x1,f . x2 are_c=-comparable by A1, A97, A102;

per cases by A107;

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

then H1 . x1,H1 . x2 are_c=-comparable by A98, A100, A103, A104, A106;
then ( H1 . x1 c= H1 . x2 or H1 . x2 c= H1 . x1 ) ;
then ( z . x1 c= z . x2 or z . x2 c= z . x1 ) by A98, A99, A103, A105, A108, XBOOLE_1:9;
hence y1,y2 are_c=-comparable by A93, A95; :: thesis:

end;

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

then A109: f . x1 c< f . x2 ;
S₂[f . x2,g . (f . x2)] by A23, A102;
then A110: f . x1 c= g . (f . x2) by A97, A109;
g . (f . x2) c= z . x2 by A105, XBOOLE_1:7;
then A111: f . x1 c= z . x2 by A110;
S₂[f . x1,g . (f . x1)] by A23, A97;
then g . (f . x1) c< f . x1 ;
then g . (f . x1) c= f . x1 ;
then A112: (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 A99, A100, XBOOLE_1:9;
then z . x1 c= z . x2 by A111, A112;
hence y1,y2 are_c=-comparable by A93, A95; :: thesis:

end;

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

then A113: f . x2 c< f . x1 ;
S₂[f . x1,g . (f . x1)] by A23, A97;
then A114: f . x2 c= g . (f . x1) by A102, A113;
g . (f . x1) c= z . x1 by A99, XBOOLE_1:7;
then A115: f . x2 c= z . x1 by A114;
S₂[f . x2,g . (f . x2)] by A23, A102;
then g . (f . x2) c< f . x2 ;
then g . (f . x2) c= f . x2 ;
then A116: (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 A105, A106, XBOOLE_1:9;
then z . x2 c= z . x1 by A115, A116;
hence y1,y2 are_c=-comparable by A93, A95; :: thesis:

end;

A117: rng z is with_non-empty_elements

proof

assume not rng z is with_non-empty_elements ; :: thesis:
then {} in rng z ;
then consider x being object such that
A118: x in dom z and
A119: z . x = {} by FUNCT_1:def 3;
set fx = f . x;
A120: x in (f . x) \ (g . (f . x)) by A32, A118;
S₁[x,f . x] by A8, A118;
then f . x in Y ;
then S₃[f . x,h . (f . x)] by A31;
then consider H being Function of ((f . x) \ (g . (f . x))),(bool ((f . x) \ (g . (f . x)))) such that
A121: h . (f . x) = H and
H is one-to-one and
A122: ( rng H is with_non-empty_elements & 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 ) ;
dom H = (f . x) \ (g . (f . x)) by FUNCT_2:def 1;
then A123: H . x in rng H by A120, FUNCT_1:def 3;
z . x = (g . (f . x)) \/ (H . x) by A45, A118, A121;
hence contradiction by A119, A122, A123; :: thesis:

end;

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

proof

let x1, x2 be object ; :: thesis:
set f1 = f . x1;
set f2 = f . x2;
assume that
A124: x1 in dom z and
A125: x2 in dom z and
A126: z . x1 = z . x2 ; :: thesis:
A127: ( z . x1 = H₁(x1) & z . x2 = H₁(x2) ) by A45, A124, A125;
S₁[x2,f . x2] by A8, A125;
then A128: f . x2 in Y ;
then S₃[f . x2,h . (f . x2)] by A31;
then consider H2 being Function of ((f . x2) \ (g . (f . x2))),(bool ((f . x2) \ (g . (f . x2)))) such that
A129: h . (f . x2) = H2 and
A130: H2 is one-to-one and
A131: ( rng H2 is with_non-empty_elements & 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 ) ;
dom H2 = (f . x2) \ (g . (f . x2)) by FUNCT_2:def 1;
then A132: x2 in dom H2 by A32, A125;
then A133: H2 . x2 in rng H2 by FUNCT_1:def 3;
then A134: g . (f . x2) misses H2 . x2 by XBOOLE_1:63, XBOOLE_1:79;
S₁[x1,f . x1] by A8, A124;
then A135: f . x1 in Y ;
then S₃[f . x1,h . (f . x1)] by A31;
then consider H1 being Function of ((f . x1) \ (g . (f . x1))),(bool ((f . x1) \ (g . (f . x1)))) such that
A136: h . (f . x1) = H1 and
H1 is one-to-one and
A137: ( rng H1 is with_non-empty_elements & 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 ) ;
dom H1 = (f . x1) \ (g . (f . x1)) by FUNCT_2:def 1;
then A138: x1 in dom H1 by A32, A124;
then A139: H1 . x1 in rng H1 by FUNCT_1:def 3;
then A140: g . (f . x1) misses H1 . x1 by XBOOLE_1:63, XBOOLE_1:79;
A141: f . x1,f . x2 are_c=-comparable by A1, A128, A135;

per cases by A141;

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

then H1 . x1 = H1 . x2 by A126, A127, A129, A134, A136, A140, XBOOLE_1:71;
hence x1 = x2 by A129, A130, A132, A136, A138, A142, FUNCT_1:def 4; :: thesis:

end;

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

S₂[f . x1,g . (f . x1)] by A23, A135;
then g . (f . x1) c< f . x1 ;
then g . (f . x1) c= f . x1 ;
then (g . (f . x1)) \/ ((f . x1) \ (g . (f . x1))) = f . x1 by XBOOLE_1:45;
then A144: H₁(x2) c= f . x1 by A126, A127, A136, A139, XBOOLE_1:9;
A145: f . x1 c< f . x2 by A143;
S₂[f . x2,g . (f . x2)] by A23, A128;
then f . x1 c= g . (f . x2) by A135, A145;
then H₁(x2) c= g . (f . x2) by A144;
then H2 . x2 c= g . (f . x2) by A129, XBOOLE_1:11;
hence x1 = x2 by A131, A133, XBOOLE_1:67, XBOOLE_1:79; :: thesis:

end;

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

S₂[f . x2,g . (f . x2)] by A23, A128;
then g . (f . x2) c< f . x2 ;
then g . (f . x2) c= f . x2 ;
then (g . (f . x2)) \/ ((f . x2) \ (g . (f . x2))) = f . x2 by XBOOLE_1:45;
then A147: H₁(x1) c= f . x2 by A126, A127, A129, A133, XBOOLE_1:9;
A148: f . x2 c< f . x1 by A146;
S₂[f . x1,g . (f . x1)] by A23, A135;
then f . x2 c= g . (f . x1) by A128, A148;
then H₁(x1) c= g . (f . x1) by A147;
then H1 . x1 c= g . (f . x1) by A136, XBOOLE_1:11;
hence x1 = x2 by A137, A139, XBOOLE_1:67, XBOOLE_1:79; :: thesis:

end;

then z is one-to-one by FUNCT_1:def 4;
then X, rng z are_equipotent by A46, WELLORD2:def 4;
hence ( Y c= rng z & rng z is with_non-empty_elements & 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 A47, A61, A89, A117, CARD_1:5; :: thesis: