let A be complex-membered set ; :: thesis: for a being Complex holds a -- A = { (a - c) where c is Complex : c in A }
let a be Complex; :: thesis: a -- A = { (a - c) where c is Complex : c in A }
A1: a -- A = { (c1 - c2) where c1, c2 is Complex : ( c1 in {a} & c2 in A ) } by Th65;
thus a -- A c= { (a - c) where c is Complex : c in A } :: according to XBOOLE_0:def 10 :: thesis: { (a - c) where c is Complex : c in A } c= a -- A

proof

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

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (a - c) where c is Complex : c in A } or e in a -- A )
assume e in { (a - c) where c is Complex : c in A } ; :: thesis: e in a -- A
then ex c being Complex st
( e = a - c & c in A ) ;
hence e in a -- A by Th160; :: thesis: verum