assume not -- A is empty ; :: thesis: contradiction
then the Element of -- A in -- A ;
then ex c being Element of COMPLEX st
( the Element of -- A = - c & c in A ) ;
hence contradiction ; :: thesis: verum