let x, y, z be Surreal; :: thesis: ( 0_No < z & x * z < y * z implies x < y )
assume that
A1: 0_No < z and
A2: x * z < y * z ; :: thesis: x < y
assume y <= x ; :: thesis: contradiction

per cases then ( y == x or y < x ) ;

suppose y == x ; :: thesis: contradiction

then y * z == x * z by Th51;
hence contradiction by A2; :: thesis: verum

end;

suppose y < x ; :: thesis: contradiction

then y * z <= x * z by A1, Th70;
hence contradiction by A2; :: thesis: verum

end;

end;