let x, y be R_eal; :: thesis: ( ( ( 0. < x & y < 0. ) or ( x < 0. & 0. < y ) ) implies x * y < 0. )
assume A1: ( ( 0. < x & y < 0. ) or ( x < 0. & 0. < y ) ) ; :: thesis: x * y < 0.

now

per cases ( ( 0. < x & y < 0. ) or ( x < 0. & 0. < y ) ) by A1;

suppose A2: ( 0. < x & y < 0. ) ; :: thesis: x * y < 0.

now

per cases ( ex a, b being Real st
( x = a & y = b & x * y = a * b ) or ( ( ( 0. < x & y = -infty ) or ( y < 0. & x = +infty ) ) & x * y = -infty ) ) by A2, Def1;

suppose ex a, b being Real st
( x = a & y = b & x * y = a * b ) ; :: thesis: x * y < 0.

then consider a, b being Real such that
A3: ( x = a & y = b & x * y = a * b ) ;
thus x * y < 0. by A2, A3, XREAL_1:134; :: thesis: verum

end;

suppose ( ( ( 0. < x & y = -infty ) or ( y < 0. & x = +infty ) ) & x * y = -infty ) ; :: thesis: x * y < 0.

hence x * y < 0. ; :: thesis: verum

end;

end;

end;

hence x * y < 0. ; :: thesis: verum

end;

suppose A4: ( x < 0. & 0. < y ) ; :: thesis: x * y < 0.

now

per cases ( ex a, b being Real st
( x = a & y = b & x * y = a * b ) or ( ( ( x < 0. & y = +infty ) or ( 0. < y & x = -infty ) ) & x * y = -infty ) ) by A4, Def1;

suppose ex a, b being Real st
( x = a & y = b & x * y = a * b ) ; :: thesis: x * y < 0.

then consider a, b being Real such that
A5: ( x = a & y = b & x * y = a * b ) ;
thus x * y < 0. by A4, A5, XREAL_1:134; :: thesis: verum

end;

suppose ( ( ( x < 0. & y = +infty ) or ( 0. < y & x = -infty ) ) & x * y = -infty ) ; :: thesis: x * y < 0.

hence x * y < 0. ; :: thesis: verum

end;

end;

end;

hence x * y < 0. ; :: thesis: verum

end;

end;

end;

hence x * y < 0. ; :: thesis: verum