let X be surreal-membered set ; :: thesis: X ++ {0_No} = X
thus X ++ {0_No} c= X :: according to XBOOLE_0:def 10 :: thesis: X c= X ++ {0_No}

proof

let xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in X ++ {0_No} or xy in X )
assume A1: xy in X ++ {0_No} ; :: thesis: xy in X
consider x, y being Surreal such that
A2: ( x in X & y in {0_No} & xy = x + y ) by A1, Def8;
y = 0_No by A2, TARSKI:def 1;
hence xy in X by A2; :: thesis: verum

end;

let xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in X or xy in X ++ {0_No} )
assume A3: xy in X ; :: thesis: xy in X ++ {0_No}
reconsider x = xy as Surreal by A3, SURREAL0:def 16;
( x + 0_No = x & 0_No in {0_No} ) by TARSKI:def 1;
hence xy in X ++ {0_No} by A3, Def8; :: thesis: verum