for x1 being Element of F_Complex
for x2 being Complex st x1 = x2 holds
- x1 = - x2