thus ( x is real implies ex c being ExtReal ex a being Complex st
( x = a & c = - a ) ) :: thesis: ( ( x = +infty implies ex b1 being ExtReal st b1 = -infty ) & ( not x is real & not x = +infty implies ex b1 being ExtReal st b1 = +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 b1 being ExtReal st b1 = -infty ) & ( not x is real & not x = +infty implies ex b1 being ExtReal st b1 = +infty ) ) ; :: thesis: verum