reconsider xx = x as Surreal by A1;
take - xx ; :: thesis: for x1 being Surreal st x1 = x holds
- xx = - x1
thus for x1 being Surreal st x1 = x holds
- xx = - x1 ; :: thesis: verum