theorem :: SURREALI:31

for x being Surreal st x is positive holds
inv x is Surreal ;