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