for x1 being Element of F_Real
for x2 being Real st x1 = x2 holds
- x1 = - x2 ;