let x, y be R_eal; :: thesis: ( x * y <> +infty & x * y <> -infty & x is not Real implies y is Real )
assume A1: ( x * y <> +infty & x * y <> -infty ) ; :: thesis: ( x is Real or y is Real )
assume A2: ( x is not Real & y is not Real ) ; :: thesis: contradiction

per cases ( ( x = +infty & y = +infty ) or ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or ( x = -infty & y = -infty ) ) by A2, XXREAL_0:14;

suppose ( x = +infty & y = +infty ) ; :: thesis: contradiction

hence contradiction by A1, EXTREAL1:def 1; :: thesis: verum

end;

suppose ( x = +infty & y = -infty ) ; :: thesis: contradiction

hence contradiction by A1, EXTREAL1:def 1; :: thesis: verum

end;

suppose ( x = -infty & y = +infty ) ; :: thesis: contradiction

hence contradiction by A1, EXTREAL1:def 1; :: thesis: verum

end;

suppose ( x = -infty & y = -infty ) ; :: thesis: contradiction

hence contradiction by A1, EXTREAL1:def 1; :: thesis: verum

end;

end;