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:13;
then - x = y1 by A2, ARYTM_0:def 7;
hence - x is real by Def1; :: thesis: verum