:: deftheorem defines _term SURREALC:def 13 :
for s, y being Surreal
for r being Real
for x being Surreal holds
( x is s,y,r _term iff ( not x - s == 0_No & omega-y (x - s) == y & omega-r (x - s) = r ) );