thus ( x is positive implies ex IT being Surreal st IT = inv x ) ; :: thesis: ( not x is positive implies ex b₁ being Surreal st - b₁ = inv (- x) )
assume not x is positive ; :: thesis: ex b₁ being Surreal st - b₁ = inv (- x)
then - x is positive by A1, SURREALR:10, SURREALR:23;
then reconsider i = inv (- x) as Surreal ;
- (- i) = i ;
hence ex b₁ being Surreal st - b₁ = inv (- x) ; :: thesis: verum