theorem Th82: :: XXREAL_3:82

for y being ExtReal holds
( not y " = 0 or y = +infty or y = -infty or y = 0 )