theorem Th177: :: MEMBER_1:177

for A being complex-membered set
for a being Complex holds A -- a = { (c - a) where c is Complex : c in A }