x + (- x) = 0
;
then consider x1, x2, y1, y2 being Element of REAL such that
A1:
x = [*x1,x2*]
and
A2:
- x = [*y1,y2*]
and
A3:
0 = [*(+ (x1,y1)),(+ (x2,y2))*]
by XCMPLX_0:def 4;
( + (x2,y2) = 0 & x2 = 0 )
by A1, A3, Lm1;
then
y2 = 0
by ARYTM_0:11;
hence
- x is real
by A2, ARYTM_0:def 5; verum