let X be set ; :: thesis: X ++ {} = {}
assume X ++ {} <> {} ; :: thesis: contradiction
then consider x being object such that
A1: x in X ++ {} by XBOOLE_0:def 1;
ex a, b being Surreal st
( a in X & b in {} & x = a + b ) by Def8, A1;
hence contradiction ; :: thesis: verum