let X, Y be set ; :: thesis: X ++ Y c= Y ++ X
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in X ++ Y or z in Y ++ X )
assume z in X ++ Y ; :: thesis: z in Y ++ X
then consider x, y being Surreal such that
A1: ( x in X & y in Y & z = x + y ) by Def8;
thus z in Y ++ X by A1, Def8; :: thesis: verum