let A, B be complex-membered set ; :: thesis: A -- B = { (c1 - c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) }
thus A -- B c= { (c1 - c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) } :: according to XBOOLE_0:def 10 :: thesis: { (c1 - c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) } c= A -- B

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in A -- B or e in { (c1 - c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) } )
assume e in A -- B ; :: thesis: e in { (c1 - c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) }
then consider c1, c2 being Complex such that
A1: e = c1 + c2 and
A2: c1 in A and
A3: c2 in -- B ;
( e = c1 - (- c2) & - c2 in B ) by A1, A3, Th12;
hence e in { (c1 - c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) } by A2; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (c1 - c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) } or e in A -- B )
assume e in { (c1 - c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) } ; :: thesis: e in A -- B
then consider c1, c2 being Complex such that
A4: ( e = c1 - c2 & c1 in A ) and
A5: c2 in B ;
- c2 in -- B by A5;
hence e in A -- B by A4; :: thesis: verum