let e be set ; :: according to MEMBERED:def 5 :: thesis: ( not e in -- A or e is integer )
assume e in -- A ; :: thesis: e is integer
then ex c being Element of COMPLEX st
( e = - c & c in A ) ;
hence e is integer ; :: thesis: verum