let x be set ; :: thesis: for k being Element of NAT st x = - k & k <> x holds
x in [:{0 },NAT :] \ {[0 ,0 ]}
let k be Element of 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;
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: y2 = 0 by A4, ARYTM_0:26;
then A7: y1 = k by A4, ARYTM_0:def 7;
+ x2,y2 = 0 by A5, ARYTM_0:26;
then A8: + x1,y1 = 0 by A5, ARYTM_0:def 7;
A9: k in omega ;

A10: now

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 A9, A7, A8, ARYTM_0:def 2, ARYTM_2:2;
A14: y9 = 0 by A13, ARYTM_2:6;
x9 = 0 by A13, ARYTM_2:6;
hence contradiction by A2, A3, A4, A6, A11, A12, A14, ARYTM_0:26; :: thesis: verum

end;

x2 = 0 by A3, ARYTM_0:26;
then A15: x1 = r by A3, ARYTM_0:def 7;
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 A9, A15, A7, A8, ARYTM_0:def 2, 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, A7, A16, A17, A19, ZFMISC_1:106;
hence x in [:{0 },NAT :] \ {[0 ,0 ]} by A20, XBOOLE_0:def 5; :: thesis: verum