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 b1 being ExtReal st b1 = 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 b1 being ExtReal st b1 = 0 ) ; :: thesis: verum