:: deftheorem defines - SURREALR:def 9 :
for x, y being Surreal holds x - y = x + (- y);