let a be real number ; :: thesis: for x9 being Element of REAL+ st x9 = a holds
09 - x9 = - a
let xx be Element of REAL+ ; :: thesis: ( xx = a implies 09 - xx = - a )
assume A1: xx = a ; :: thesis: 09 - xx = - a

per cases ( xx = 0 or xx <> 0 ) ;

suppose xx = 0 ; :: thesis: 09 - xx = - a

hence 09 - xx = - a by A1, ARYTM_1:18; :: thesis: verum

end;

suppose A2: xx <> 0 ; :: thesis: 09 - xx = - a

set b = 09 - xx;
A3: 09 <=' xx by ARYTM_1:6;
then not xx <=' 09 by A2, ARYTM_1:4;
then A4: 09 - xx = [{} ,(xx -' 09)] by ARYTM_1:def 2;

now

assume 09 - xx = [0 ,0 ] ; :: thesis: contradiction
then xx -' 09 = 0 by A4, ZFMISC_1:33;
hence contradiction by A2, A3, ARYTM_1:10; :: thesis: verum

end;

then A5: not 09 - xx in {[0 ,0 ]} by TARSKI:def 1;
A6: xx -' 09 = (xx -' 09) + 09 by ARYTM_2:def 8
.= xx by A3, ARYTM_1:def 1 ;
0 in {0 } by TARSKI:def 1;
then A7: 09 - xx in [:{0 },REAL+ :] by A4, ZFMISC_1:106;
then 09 - xx in REAL+ \/ [:{0 },REAL+ :] by XBOOLE_0:def 3;
then reconsider b = 09 - xx as Element of REAL by A5, NUMBERS:def 1, XBOOLE_0:def 5;
consider x1, x2, y1, y2 being Element of REAL such that
A8: a = [*x1,x2*] and
A9: b = [*y1,y2*] and
A10: a + b = [*(+ x1,y1),(+ x2,y2)*] by XCMPLX_0:def 4;
+ x2,y2 = 0 by A10, ARYTM_0:26;
then A11: a + b = + x1,y1 by A10, ARYTM_0:def 7;
a in REAL by XREAL_0:def 1;
then x2 = 0 by A8, ARYTM_0:26;
then A12: a = x1 by A8, ARYTM_0:def 7;
y2 = 0 by A9, ARYTM_0:26;
then A13: b = y1 by A9, ARYTM_0:def 7;
then consider x9, y9 being Element of REAL+ such that
A14: x1 = x9 and
A15: y1 = [0 ,y9] and
A16: + x1,y1 = x9 - y9 by A1, A7, A12, ARYTM_0:def 2;
y9 = xx -' 09 by A4, A13, A15, ZFMISC_1:33;
then a + b = 0 by A1, A12, A11, A14, A16, A6, ARYTM_1:18;
hence 09 - xx = - a ; :: thesis: verum

end;

end;