let z be object ; :: according to SURREAL0:def 16 :: thesis: ( not z in X ++ Y or z is surreal )
assume z in X ++ Y ; :: thesis: z is surreal
then ex x, y being Surreal st
( x in X & y in Y & x + y = z ) by Def8;
hence z is surreal ; :: thesis: verum