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

per cases ( x <= 0_No or 0_No < x ) ;

suppose x <= 0_No ; :: thesis: y * x <= z * x

then x == 0_No by A1;
then ( y * x == y * 0_No & y * 0_No = 0_No & 0_No = z * 0_No & z * 0_No == z * x ) by Th51;
hence y * x <= z * x by SURREALO:4; :: thesis: verum

end;

suppose A2: 0_No < x ; :: thesis: y * x <= z * x

per cases ( z <= y or y < z ) ;

suppose z <= y ; :: thesis: y * x <= z * x

then z == y by A1;
then y * x == z * x by Th51;
hence y * x <= z * x ; :: thesis: verum

end;

suppose y < z ; :: thesis: y * x <= z * x

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

end;

end;

end;

end;