let X be non empty set ; :: thesis: ex Y being Subset-Family of X st
( Y is with_non-empty_elements & Y is c=-linear & X in Y & card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
consider R being Relation such that
A1: R well_orders X by WELLORD2:17;
set RX = R |_2 X;
deffunc H1( object ) -> Element of bool X = X \ ((R |_2 X) -Seg $1);
A2: for x being object st x in X holds
H1(x) in bool X ;
consider f being Function of X,(bool X) such that
A3: for x being object st x in X holds
f . x = H1(x) from FUNCT_2:sch 2(A2);
 take Y = rng f; :: thesis: ( Y is with_non-empty_elements & Y is c=-linear & X in Y & card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
A4: dom f = X by FUNCT_2:def 1;
thus Y is with_non-empty_elements :: thesis: ( Y is c=-linear & X in Y & card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
proof
assume Y is with_empty_element ; :: thesis: contradiction
then {} in Y ;
then consider x being object such that
A5: x in dom f and
A6: f . x = {} by FUNCT_1:def 3;
{} = H1(x) by A3, A5, A6;
then X c= (R |_2 X) -Seg x by XBOOLE_1:37;
hence contradiction by A4, A5, WELLORD1:1; :: thesis: verum
end;
thus Y is c=-linear :: thesis: ( X in Y & card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
proof
let x be set ; :: according to ORDINAL1:def 8 :: thesis: for b1 being set holds
( not x in Y or not b1 in Y or x,b1 are_c=-comparable )
let y be set ; :: thesis: ( not x in Y or not y in Y or x,y are_c=-comparable )
assume that
A7: x in Y and
A8: y in Y ; :: thesis: x,y are_c=-comparable
consider a being object such that
A9: ( a in dom f & f . a = x ) by A7, FUNCT_1:def 3;
consider b being object such that
A10: ( b in dom f & f . b = y ) by A8, FUNCT_1:def 3;
(R |_2 X) -Seg a,(R |_2 X) -Seg b are_c=-comparable by A1, WELLORD1:26, WELLORD2:16;
then ( (R |_2 X) -Seg a c= (R |_2 X) -Seg b or (R |_2 X) -Seg b c= (R |_2 X) -Seg a ) ;
then ( H1(b) c= H1(a) or H1(a) c= H1(b) ) by XBOOLE_1:34;
then A11: H1(a),H1(b) are_c=-comparable ;
x = H1(a) by A3, A9;
hence x,y are_c=-comparable by A3, A10, A11; :: thesis: verum
end;
A12: field (R |_2 X) = X by A1, WELLORD2:16;
then consider x being object such that
A13: x in X and
A14: for y being object st y in X holds
[x,y] in R |_2 X by A1, WELLORD1:7, WELLORD2:16;
A15: R |_2 X is well-ordering by A1, WELLORD2:16;
then A16: R |_2 X is well_founded by WELLORD1:def 4;
R |_2 X is antisymmetric by A15, WELLORD1:def 4;
then A17: R |_2 X is_antisymmetric_in X by A12, RELAT_2:def 12;
A18: (R |_2 X) -Seg x = {}
proof
assume (R |_2 X) -Seg x <> {} ; :: thesis: contradiction
then consider y being object such that
A19: y in (R |_2 X) -Seg x by XBOOLE_0:def 1;
A20: y <> x by A19, WELLORD1:1;
A21: [y,x] in R |_2 X by A19, WELLORD1:1;
then A22: x in X by A12, RELAT_1:15;
A23: y in X by A12, A21, RELAT_1:15;
then [x,y] in R |_2 X by A14;
hence contradiction by A17, A20, A21, A22, A23, RELAT_2:def 4; :: thesis: verum
end;
f . x = H1(x) by A3, A13;
hence X in Y by A4, A13, A18, FUNCT_1:def 3; :: thesis: ( card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
now :: thesis: for x1, x2 being object st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in X & x2 in X & f . x1 = f . x2 implies x1 = x2 )
reconsider R1 = (R |_2 X) -Seg x1, R2 = (R |_2 X) -Seg x2 as Subset of X by A12, WELLORD1:9;
assume that
A24: ( x1 in X & x2 in X ) and
A25: f . x1 = f . x2 ; :: thesis: x1 = x2
( R1 ` = f . x1 & f . x2 = R2 ` ) by A3, A24;
then R1 = R2 by A25, SUBSET_1:42;
then ( [x1,x2] in R |_2 X & [x2,x1] in R |_2 X ) by A12, A15, A24, WELLORD1:29;
hence x1 = x2 by A17, A24, RELAT_2:def 4; :: thesis: verum
end;
then f is one-to-one by FUNCT_2:19;
then X,Y are_equipotent by A4, WELLORD2:def 4;
hence card X = card Y by CARD_1:5; :: thesis: for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y )
let Z be set ; :: thesis: ( Z in Y & card Z <> 1 implies ex x being set st
( x in Z & Z \ {x} in Y ) )
assume that
A26: Z in Y and
A27: card Z <> 1 ; :: thesis: ex x being set st
( x in Z & Z \ {x} in Y )
consider x being object such that
A28: x in dom f and
A29: f . x = Z by A26, FUNCT_1:def 3;
A30: {x} c= X by A28, ZFMISC_1:31;
reconsider x = x as set by TARSKI:1;
take x ; :: thesis: ( x in Z & Z \ {x} in Y )
A31: not x in (R |_2 X) -Seg x by WELLORD1:1;
A32: Z = X \ ((R |_2 X) -Seg x) by A3, A28, A29;
hence x in Z by A28, A31, XBOOLE_0:def 5; :: thesis: Z \ {x} in Y
(R |_2 X) -Seg x c= X by A12, WELLORD1:9;
then reconsider Rxx = ((R |_2 X) -Seg x) \/ {x} as Subset of X by A30, XBOOLE_1:8;
X \ Rxx <> {}
proof
assume X \ Rxx = {} ; :: thesis: contradiction
then X c= Rxx by XBOOLE_1:37;
then Z = Rxx \ ((R |_2 X) -Seg x) by A32, XBOOLE_0:def 10
.= {x} \ ((R |_2 X) -Seg x) by XBOOLE_1:40
.= {x} by A31, ZFMISC_1:59 ;
hence contradiction by A27, CARD_1:30; :: thesis: verum
end;
then consider a being object such that
A33: a in Rxx ` and
A34: (R |_2 X) -Seg a misses Rxx ` by A12, A16, WELLORD1:def 2;
A35: not a in Rxx by A33, XBOOLE_0:def 5;
x in {x} by TARSKI:def 1;
then A36: x <> a by A35, XBOOLE_0:def 3;
R |_2 X is connected by A15, WELLORD1:def 4;
then R |_2 X is_connected_in X by A12, RELAT_2:def 14;
then A37: ( [x,a] in R |_2 X or [a,x] in R |_2 X ) by A28, A33, A36, RELAT_2:def 6;
A38: not a in (R |_2 X) -Seg x by A35, XBOOLE_0:def 3;
then x in (R |_2 X) -Seg a by A36, A37, WELLORD1:1;
then A39: {x} c= (R |_2 X) -Seg a by ZFMISC_1:31;
(R |_2 X) -Seg a c= X by A12, WELLORD1:9;
then A40: (R |_2 X) -Seg a c= Rxx by A34, SUBSET_1:24;
(R |_2 X) -Seg x c= (R |_2 X) -Seg a by A12, A15, A28, A33, A37, A38, WELLORD1:1, WELLORD1:29;
then Rxx c= (R |_2 X) -Seg a by A39, XBOOLE_1:8;
then Rxx = (R |_2 X) -Seg a by A40;
then f . a = X \ Rxx by A3, A33
.= (X \ ((R |_2 X) -Seg x)) \ {x} by XBOOLE_1:41
.= Z \ {x} by A3, A28, A29 ;
hence Z \ {x} in Y by A4, A33, FUNCT_1:def 3; :: thesis: verum