let x be ExtReal; :: thesis: ( ( x = +infty implies - x = -infty ) & ( - x = -infty implies x = +infty ) & ( x = -infty implies - x = +infty ) & ( - x = +infty implies x = -infty ) )
( - x = +infty implies x = -infty )

proof

assume - x = +infty ; :: thesis: x = -infty
then - (- x) = -infty by Def3;
hence x = -infty ; :: thesis: verum

end;

hence ( ( x = +infty implies - x = -infty ) & ( - x = -infty implies x = +infty ) & ( x = -infty implies - x = +infty ) & ( - x = +infty implies x = -infty ) ) by Th5; :: thesis: verum