let x be object ; :: thesis: for k being Nat st x = - k & k <> x holds
x in [:{0},NAT:] \ {[0,0]}
let k be Nat; :: thesis: ( x = - k & k <> x implies x in [:{0},NAT:] \ {[0,0]} )
assume that
A1: x = - k and
A2: k <> x ; :: thesis: x in [:{0},NAT:] \ {[0,0]}
reconsider r = x as Element of REAL by A1, XREAL_0:def 1;
r + k = 0 by A1;
then consider x1, x2, y1, y2 being Element of REAL such that
A3: r = [*x1,x2*] and
A4: k = [*y1,y2*] and
A5: 0 = [*(+ (x1,y1)),(+ (x2,y2))*] by XCMPLX_0:def 4;
A6: k in NAT by ORDINAL1:def 12;
then k in REAL by NUMBERS:19;
then A7: y2 = 0 by A4, ARYTM_0:24;
then A8: y1 = k by A4, ARYTM_0:def 5;
+ (x2,y2) = In (0,REAL) by A5, ARYTM_0:24;
then A9: + (x1,y1) = 0 by A5, ARYTM_0:def 5;

A10: now :: thesis: not x1 in REAL+

assume x1 in REAL+ ; :: thesis: contradiction
then consider x9, y9 being Element of REAL+ such that
A11: x1 = x9 and
A12: y1 = y9 and
A13: 0 = x9 + y9 by A6, A8, A9, ARYTM_0:def 1, ARYTM_2:2;
A14: y9 = 0 by A13, ARYTM_2:5;
x9 = 0 by A13, ARYTM_2:5;
hence contradiction by A2, A3, A4, A7, A11, A12, A14, ARYTM_0:24; :: thesis: verum

end;

x2 = 0 by A3, ARYTM_0:24;
then A15: x1 = r by A3, ARYTM_0:def 5;
r in REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1, XBOOLE_0:def 5;
then x in [:{0},REAL+:] by A15, A10, XBOOLE_0:def 3;
then consider x9, y9 being Element of REAL+ such that
A16: x1 = [0,x9] and
A17: y1 = y9 and
A18: 0 = y9 - x9 by A6, A15, A8, A9, ARYTM_0:def 1, ARYTM_2:2;
A19: 0 in {0} by TARSKI:def 1;
A20: not r in {[0,0]} by NUMBERS:def 1, XBOOLE_0:def 5;
x9 = y9 by A18, ARYTM_0:6;
then x in [:{0},NAT:] by A15, A8, A16, A17, A19, ZFMISC_1:87, A6;
hence x in [:{0},NAT:] \ {[0,0]} by A20, XBOOLE_0:def 5; :: thesis: verum