for x, y being ExtReal st x * y <> +infty & x * y <> -infty & not x in REAL holds
y in REAL