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; :: thesis: verum

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; :: thesis: verum