per cases ( x = 0 or y = 0 or ( x < 0 & y > 0 ) ) ;

suppose ( x = 0 or y = 0 ) ; :: thesis: not x * y is positive

hence x * y <= 0 by Lm17; :: according to XXREAL_0:def 6 :: thesis: verum

end;

suppose ( x < 0 & y > 0 ) ; :: thesis: not x * y is positive

hence x * y <= 0 ; :: according to XXREAL_0:def 6 :: thesis: verum

end;

end;