let x be Surreal; :: thesis: x + 0_No = x
set y = 0_No ;
defpred S₁[ Ordinal] means for x being Surreal st born x = $1 holds
x + 0_No = x;
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
let x be Surreal; :: thesis: ( born x = D implies x + 0_No = x )
assume A3: born x = D ; :: thesis: x + 0_No = x
( {x} ++ (L_ 0_No) = {} & {x} ++ (R_ 0_No) = {} ) by Th27;
then A4: ( ((L_ x) ++ {0_No}) \/ ({x} ++ (L_ 0_No)) = (L_ x) ++ {0_No} & ((R_ x) ++ {0_No}) \/ ({x} ++ (R_ 0_No)) = (R_ x) ++ {0_No} ) ;
A5: for Y being set st Y c= (L_ x) \/ (R_ x) holds
Y ++ {0_No} = Y

proof

let Y be set ; :: thesis: ( Y c= (L_ x) \/ (R_ x) implies Y ++ {0_No} = Y )
assume A6: Y c= (L_ x) \/ (R_ x) ; :: thesis: Y ++ {0_No} = Y
thus Y ++ {0_No} c= Y :: according to XBOOLE_0:def 10 :: thesis: Y c= Y ++ {0_No}

proof

let xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in Y ++ {0_No} or xy in Y )
assume A7: xy in Y ++ {0_No} ; :: thesis: xy in Y
consider x1, y1 being Surreal such that
A8: ( x1 in Y & y1 in {0_No} & xy = x1 + y1 ) by A7, Def8;
y1 = 0_No by A8, TARSKI:def 1;
hence xy in Y by A2, A8, A6, SURREALO:1, A3; :: thesis: verum

end;

let xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in Y or xy in Y ++ {0_No} )
assume A9: xy in Y ; :: thesis: xy in Y ++ {0_No}
then reconsider xy = xy as Surreal by SURREAL0:def 16, A6;
A10: 0_No in {0_No} by TARSKI:def 1;
xy + 0_No = xy by A2, A9, A6, A3, SURREALO:1;
hence xy in Y ++ {0_No} by A10, A9, Def8; :: thesis: verum

end;

( (L_ x) ++ {0_No} = L_ x & (R_ x) ++ {0_No} = R_ x ) by XBOOLE_1:7, A5;
then x + 0_No = [(L_ x),(R_ x)] by A4, Th28;
hence x + 0_No = x ; :: thesis: verum

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
hence x + 0_No = x ; :: thesis: verum