let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in comp (X,x,y,Y) or o is surreal )
assume o in comp (X,x,y,Y) ; :: thesis: o is surreal
then ex x1, y1 being Surreal st
( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) by Def14;
hence o is surreal ; :: thesis: verum