thus ( x is real implies ex c being ExtReal ex a being Complex st
( x = a & c = - a ) ) :: thesis: ( ( x = +infty implies ex b₁ being ExtReal st b₁ = -infty ) & ( not x is real & not x = +infty implies ex b₁ being ExtReal st b₁ = +infty ) )

proof

assume x is real ; :: thesis: ex c being ExtReal ex a being Complex st
( x = a & c = - a )
then reconsider a = x as Real ;
take - a ; :: thesis: ex a being Complex st
( x = a & - a = - a )
take a ; :: thesis: ( x = a & - a = - a )
thus ( x = a & - a = - a ) ; :: thesis: verum

end;

thus ( ( x = +infty implies ex b₁ being ExtReal st b₁ = -infty ) & ( not x is real & not x = +infty implies ex b₁ being ExtReal st b₁ = +infty ) ) ; :: thesis: verum