let x, y be Surreal; :: thesis: {x} ++ {y} = {(x + y)}
thus {x} ++ {y} c= {(x + y)} :: according to XBOOLE_0:def 10 :: thesis: {(x + y)} c= {x} ++ {y}

proof

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

end;

A2: ( x in {x} & y in {y} ) by TARSKI:def 1;
for o being object st o in {(x + y)} holds
o in {x} ++ {y}

proof

let o be object ; :: thesis: ( o in {(x + y)} implies o in {x} ++ {y} )
assume o in {(x + y)} ; :: thesis: o in {x} ++ {y}
then o = x + y by TARSKI:def 1;
hence o in {x} ++ {y} by A2, Def8; :: thesis: verum

end;

hence {(x + y)} c= {x} ++ {y} by TARSKI:def 3; :: thesis: verum