:: deftheorem defines - SURREALR:def 3 :
for x being Surreal holds - x = (No_opposite_op (born x)) . x;