let x, y be Element of REAL+ ; :: thesis: ( x <=' y implies ex z being Element of REAL+ st x + z = y )
assume A1: x <=' y ; :: thesis: ex z being Element of REAL+ st x + z = y
per cases ( x = {} or x = y or ( x <> {} & x <> y ) ) ;
suppose A2: x = {} ; :: thesis: ex z being Element of REAL+ st x + z = y
take y ; :: thesis: x + y = y
thus x + y = y by A2, Def8; :: thesis: verum
end;
suppose A3: x = y ; :: thesis: ex z being Element of REAL+ st x + z = y
reconsider z = {} as Element of REAL+ by Th1;
take z ; :: thesis: x + z = y
thus x + z = y by A3, Def8; :: thesis: verum
end;
suppose that A4: x <> {} and
A5: x <> y ; :: thesis: ex z being Element of REAL+ st x + z = y
A6: DEDEKIND_CUT x <> {} by A4, Lm10;
DEDEKIND_CUT x <> DEDEKIND_CUT y by A5, Lm22;
then consider C being Element of DEDEKIND_CUTS such that
A7: (DEDEKIND_CUT x) + C = DEDEKIND_CUT y by A1, A6, Lm36, Lm37;
take GLUED C ; :: thesis: x + (GLUED C) = y
now :: thesis: not C = {}
assume A8: C = {} ; :: thesis: contradiction
for e being object holds not e in { (r + s) where r, s is Element of RAT+ : ( r in C & s in DEDEKIND_CUT x ) }
proof
given e being object such that A9: e in { (r + s) where r, s is Element of RAT+ : ( r in C & s in DEDEKIND_CUT x ) } ; :: thesis: contradiction
ex r, s being Element of RAT+ st
( e = r + s & r in C & s in DEDEKIND_CUT x ) by A9;
hence contradiction by A8; :: thesis: verum
end;
then { (r + s) where r, s is Element of RAT+ : ( r in C & s in DEDEKIND_CUT x ) } = {} by XBOOLE_0:def 1;
then DEDEKIND_CUT y = {} by A7, Def6;
hence contradiction by A1, A6, Lm37, XBOOLE_1:3; :: thesis: verum
end;
then GLUED C <> {} by Lm11;
hence x + (GLUED C) = GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT (GLUED C))) by A4, Def8
.= GLUED (DEDEKIND_CUT y) by A7, Lm12
.= y by Lm23 ;
:: thesis: verum
end;
end;