theorem :: XXREAL_3:89

for y being ExtReal holds
( +infty * y <> 1 & -infty * y <> 1 )