theorem :: XXREAL_3:89
for y being ExtReal holds
( +infty * y <> 1 & -infty * y <> 1 )