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

now

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

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

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

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

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

end;

end;

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