assume A1: - x = 0 ; :: according to ORDINAL1:def 14 :: thesis: contradiction
x + (- x) = 0 by Def5;
then consider x1, x2, y1, y2 being Element of REAL such that
A2: x = [*x1,x2*] and
A3: - x = [*y1,y2*] and
A4: In (0,REAL) = [*(+ (x1,y1)),(+ (x2,y2))*] by Def3, Lm1;
A5: + (x2,y2) = 0 by A4, ARYTM_0:24;
then A6: + (x1,y1) = 0 by A4, ARYTM_0:def 5, Lm1;
y2 = In (0,REAL) by A1, A3, ARYTM_0:24, Lm1;
then A7: y1 = 0 by A1, A3, ARYTM_0:def 5, Lm1;
x2 = 0 by A1, A3, A5, ARYTM_0:11, ARYTM_0:24;
then x = x1 by A2, ARYTM_0:def 5
.= 0 by A6, A7, ARYTM_0:11 ;
hence contradiction ; :: thesis: verum