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