let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in divset (X,x,Y) or o is surreal )
assume o in divset (X,x,Y) ; :: thesis: o is surreal
then ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) by Def15;
hence o is surreal ; :: thesis: verum