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