theorem :: SURREALI:32

for x, y being Surreal st x is positive & y = inv x holds
x * y == 1_No by Lm2;