:: deftheorem defines inv SURREALI:def 12 :
for x being Surreal holds inv x = (No_inverse_op (born x)) . x;