let x, y be Surreal; :: thesis: for X, Y being set holds comp (X,x,y,Y) c= comp (Y,y,x,X)
let X, Y be set ; :: thesis: comp (X,x,y,Y) c= comp (Y,y,x,X)
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in comp (X,x,y,Y) or o in comp (Y,y,x,X) )
assume o in comp (X,x,y,Y) ; :: thesis: o in comp (Y,y,x,X)
then consider x1, y1 being Surreal such that
A1: ( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) by Def14;
o = ((x1 * y) + (x * y1)) + (- (x1 * y1)) by A1
.= ((y1 * x) + (y * x1)) + (- (y1 * x1)) ;
hence o in comp (Y,y,x,X) by A1, Def14; :: thesis: verum