let e be object ; :: according to MEMBERED:def 3 :: thesis: ( not e in -- A or e is real )
assume e in -- A ; :: thesis: e is real
then ex c being Complex st
( e = - c & c in A ) ;
hence e is real ; :: thesis: verum