for x being ExtReal
for a being Real st x = a holds
- x = - a by XXREAL_3:def 3;