let x, y be ext-real number ; :: thesis: ( x * y <> +infty & x * y <> -infty & not x in REAL implies y in REAL )
assume A1: ( x * y <> +infty & x * y <> -infty ) ; :: thesis: ( x in REAL or y in REAL )
assume A2: ( not x in REAL & not y in 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, Def4; :: thesis: verum

end;

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

hence contradiction by A1, Def4; :: thesis: verum

end;

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

hence contradiction by A1, Def4; :: thesis: verum

end;

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

hence contradiction by A1, Def4; :: thesis: verum

end;

end;