let x, y be Surreal; :: thesis: ( ( ( x < 0_No & 0_No < y ) or ( 0_No < x & y < 0_No ) ) iff x * y < 0_No )
set z = - y;
thus ( not x * y < 0_No or ( x < 0_No & 0_No < y ) or ( 0_No < x & y < 0_No ) ) :: thesis: ( ( ( x < 0_No & 0_No < y ) or ( 0_No < x & y < 0_No ) ) implies x * y < 0_No )

proof

assume x * y < 0_No ; :: thesis: ( ( x < 0_No & 0_No < y ) or ( 0_No < x & y < 0_No ) )
then ( 0_No < - (x * y) & - (x * y) = x * (- y) ) by Th23, Th10, Th58;
then ( ( x < 0_No & - y < 0_No ) or ( 0_No < x & 0_No < - y ) ) by Th72;
hence ( ( x < 0_No & 0_No < y ) or ( 0_No < x & y < 0_No ) ) by Th23, Th10; :: thesis: verum

end;

assume ( ( x < 0_No & 0_No < y ) or ( 0_No < x & y < 0_No ) ) ; :: thesis: x * y < 0_No
then ( ( x < 0_No & - y < 0_No ) or ( 0_No < x & 0_No < - y ) ) by Th23, Th10;
then ( 0_No < x * (- y) & x * (- y) = - (x * y) ) by Th72, Th58;
hence x * y < 0_No by Th23, Th10; :: thesis: verum