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