let x, y, z be Surreal; :: thesis: ( 0_No < x & y < z implies y * x < z * x )
assume ( 0_No < x & y < z ) ; :: thesis: y * x < z * x
then (0_No * z) + (x * y) < (0_No * y) + (x * z) by Th51;
hence y * x < z * x ; :: thesis: verum