reconsider z' = 0 as Element of REAL+ by ARYTM_2:21;
A1:
( x in REAL+ \/ [:{0 },REAL+ :] & not x in {[0 ,0 ]} )
by NUMBERS:def 1, XBOOLE_0:def 5;
per cases
( x = 0 or ( x in REAL+ & x <> 0 ) or x in [:{0 },REAL+ :] )
by A1, XBOOLE_0:def 3;
suppose that A3:
x in REAL+
and A4:
x <> 0
;
:: thesis: ex b1 being Element of REAL st + x,b1 = 0
0 in {0 }
by TARSKI:def 1;
then A5:
[0 ,x] in [:{0 },REAL+ :]
by A3, ZFMISC_1:106;
then A6:
[0 ,x] in REAL+ \/ [:{0 },REAL+ :]
by XBOOLE_0:def 3;
[0 ,x] <> [0 ,0 ]
by A4, ZFMISC_1:33;
then reconsider y =
[0 ,x] as
Element of
REAL by A6, NUMBERS:def 1, ZFMISC_1:64;
take
y
;
:: thesis: + x,y = 0 reconsider x' =
x as
Element of
REAL+ by A3;
A7:
x' <=' x'
;
z' + x' = x'
by ARYTM_2:def 8;
then
z' = x' -' x'
by A7, ARYTM_1:def 1;
then
0 = x' - x'
by A7, ARYTM_1:def 2;
hence
+ x,
y = 0
by A5, Def2;
:: thesis: verum end;