let y be ExtReal; :: thesis: ( +infty * y <> 1 & -infty * y <> 1 )
( y = 0 or 0 < y or y < 0 ) ;
hence ( +infty * y <> 1 & -infty * y <> 1 ) by Def5; :: thesis: verum