let x be Surreal; :: thesis: ( not x == 0_No implies (x ") " == x )
assume not x == 0_No ; :: thesis: (x ") " == x
then A1: ( 0_No < 1_No & 1_No == x * (x ") ) by Th33, Def8;
then not x * (x ") == 0_No by SURREALO:4;
then not x " == 0_No by SURREALR:72, SURREALR:74;
hence (x ") " == x by A1, Th41; :: thesis: verum