:: deftheorem Def15 defines divset SURREALI:def 15 :
for X, Y being set
for x being Surreal
for b₄ being set holds
( b₄ = divset (X,x,Y) iff for o being object holds
( o in b₄ iff ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) ) );