let x be Surreal; :: thesis: ( not x == 0_No implies x * (x ") == 1_No )
assume A1: not x == 0_No ; :: thesis: x * (x ") == 1_No

per cases ( 0_No < x or not 0_No < x ) ;

suppose 0_No < x ; :: thesis: x * (x ") == 1_No

then A2: x is positive ;
then x " = inv x by A1, Def14;
hence x * (x ") == 1_No by A2, Lm2; :: thesis: verum

end;

suppose A3: not 0_No < x ; :: thesis: x * (x ") == 1_No

then A4: - x is positive by A1, SURREALR:23, SURREALR:10;
then reconsider I = inv (- x) as Surreal ;
A5: not x is positive by A3;
(x ") * x = (- (x ")) * (- x) by SURREALR:58
.= I * (- x) by A5, A1, Def14 ;
hence x * (x ") == 1_No by A4, Lm2; :: thesis: verum

end;

end;