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