let x, y be ExtReal; :: thesis: ( x * y <> +infty & x * y <> -infty & not x in REAL implies y in REAL )
assume that
A1: x * y <> +infty and
A2: x * y <> -infty ; :: thesis: ( x in REAL or y in REAL )
assume A3: ( 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 A3, XXREAL_0:14;

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

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

end;

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

hence contradiction by A2, Def5; :: thesis: verum

end;

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

hence contradiction by A2, Def5; :: thesis: verum

end;

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

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

end;

end;