let x be Surreal; :: thesis: ( not x == 0_No implies ( 0_No < x iff 0_No < x " ) )
assume not x == 0_No ; :: thesis: ( 0_No < x iff 0_No < x " )
then A1: x * (x ") == 1_No by Th33;
A2: 0_No < x * (x ") by A1, SURREALO:4, Def8;
thus ( 0_No < x implies 0_No < x " ) :: thesis: ( 0_No < x " implies 0_No < x )

proof

assume 0_No < x ; :: thesis: 0_No < x "
then 0_No <= x ;
hence 0_No < x " by A2, SURREALR:72; :: thesis: verum

end;

assume 0_No < x " ; :: thesis: 0_No < x
then 0_No <= x " ;
hence 0_No < x by A2, SURREALR:72; :: thesis: verum