theorem Th23: :: XXREAL_3:23

for x being ExtReal holds
( ( x = +infty implies - x = -infty ) & ( - x = -infty implies x = +infty ) & ( x = -infty implies - x = +infty ) & ( - x = +infty implies x = -infty ) )