{ (- c) where c is Element of COMPLEX : c in A } is complex-membered

proof

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

end;

hence { (- c) where c is Element of COMPLEX : c in A } is complex-membered set ; :: thesis: verum