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

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 ( not x is real implies ex b₁ being ExtReal st b₁ = 0 ) ; :: thesis: verum