let A be complex-membered set ; :: thesis: 0 ** A c= {0}
let a be Complex; :: according to MEMBERED:def 7 :: thesis: ( not a in 0 ** A or a in {0} )
assume a in 0 ** A ; :: thesis: a in {0}
then consider c1, c2 being Complex such that
A1: a = c1 * c2 and
A2: c1 in {0} and
c2 in A ;
c1 = 0 by A2, TARSKI:def 1;
hence a in {0} by A1, TARSKI:def 1; :: thesis: verum