let X be set ; :: thesis: card (-- X) c= card X
defpred S₁[ object , object ] means for x being Surreal st x = $1 holds
$2 = - x;
A1: for o being object st o in -- X holds
ex u being object st S₁[o,u]

proof

let o be object ; :: thesis: ( o in -- X implies ex u being object st S₁[o,u] )
assume o in -- X ; :: thesis: ex u being object st S₁[o,u]
then consider x being Surreal such that
A2: ( x in X & o = - x ) by Def4;
take x ; :: thesis: S₁[o,x]
let y be Surreal; :: thesis: ( y = o implies x = - y )
thus ( y = o implies x = - y ) by A2; :: thesis: verum

end;

consider f being Function such that
A3: dom f = -- X and
A4: for o being object st o in -- X holds
S₁[o,f . o] from CLASSES1:sch 1(A1);
A5: rng f c= X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in X )
assume y in rng f ; :: thesis: y in X
then consider x being object such that
A6: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
consider z being Surreal such that
A7: ( z in X & x = - z ) by A3, A6, Def4;
( f . x = - (- z) & - (- z) = z ) by A6, A7, A3, A4;
hence y in X by A7, A6; :: thesis: verum

end;

f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume A8: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
consider y1 being Surreal such that
A9: ( y1 in X & x1 = - y1 ) by A8, A3, Def4;
consider y2 being Surreal such that
A10: ( y2 in X & x2 = - y2 ) by A8, A3, Def4;
( f . x1 = - (- y1) & - (- y1) = y1 & f . x2 = - (- y2) & - (- y2) = y2 ) by A10, A9, A3, A8, A4;
hence x1 = x2 by A8, A9, A10; :: thesis: verum

end;

hence card (-- X) c= card X by CARD_1:10, A3, A5; :: thesis: verum