let x, y be Surreal; :: thesis: for X, Y being set holds comp (X,x,y,Y) = comp (Y,y,x,X)
let X, Y be set ; :: thesis: comp (X,x,y,Y) = comp (Y,y,x,X)
( comp (X,x,y,Y) c= comp (Y,y,x,X) & comp (Y,y,x,X) c= comp (X,x,y,Y) ) by Lm6;
hence comp (X,x,y,Y) = comp (Y,y,x,X) by XBOOLE_0:def 10; :: thesis: verum