let x, y be Element of REAL+ ; :: thesis: ( x in RAT+ & y in RAT+ implies ex x', y' being Element of RAT+ st
( x = x' & y = y' & x + y = x' + y' ) )
assume that
A1: x in RAT+ and
A2: y in RAT+ ; :: thesis: ex x', y' being Element of RAT+ st
( x = x' & y = y' & x + y = x' + y' )

per cases ( x = {} or y = {} or ( y <> {} & x <> {} ) ) ;

suppose A3: x = {} ; :: thesis: ex x', y' being Element of RAT+ st
( x = x' & y = y' & x + y = x' + y' )

reconsider y' = y as Element of RAT+ by A2;
take {} ; :: thesis: ex y' being Element of RAT+ st
( x = {} & y = y' & x + y = {} + y' )
take y' ; :: thesis: ( x = {} & y = y' & x + y = {} + y' )
thus x = {} by A3; :: thesis: ( y = y' & x + y = {} + y' )
thus y = y' ; :: thesis: x + y = {} + y'
thus x + y = y by A3, Def8
.= {} + y' by ARYTM_3:56 ; :: thesis: verum

end;

suppose A4: y = {} ; :: thesis: ex x', y' being Element of RAT+ st
( x = x' & y = y' & x + y = x' + y' )

reconsider x' = x as Element of RAT+ by A1;
take x' ; :: thesis: ex y' being Element of RAT+ st
( x = x' & y = y' & x + y = x' + y' )
take {} ; :: thesis: ( x = x' & y = {} & x + y = x' + {} )
thus x = x' ; :: thesis: ( y = {} & x + y = x' + {} )
thus y = {} by A4; :: thesis: x + y = x' + {}
thus x + y = x by A4, Def8
.= x' + {} by ARYTM_3:56 ; :: thesis: verum

end;

suppose that A5: y <> {} and
A6: x <> {} ; :: thesis: ex x', y' being Element of RAT+ st
( x = x' & y = y' & x + y = x' + y' )

consider x' being Element of RAT+ such that
A7: x = x' and
A8: DEDEKIND_CUT x = { s where s is Element of RAT+ : s < x' } by A1, Def3;
consider y' being Element of RAT+ such that
A9: y = y' and
A10: DEDEKIND_CUT y = { s where s is Element of RAT+ : s < y' } by A2, Def3;
take x' ; :: thesis: ex y' being Element of RAT+ st
( x = x' & y = y' & x + y = x' + y' )
take y' ; :: thesis: ( x = x' & y = y' & x + y = x' + y' )
thus ( x = x' & y = y' ) by A7, A9; :: thesis: x + y = x' + y'
set A = DEDEKIND_CUT x;
set B = DEDEKIND_CUT y;
A11: for s being Element of RAT+ holds
( s in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) iff s < x' + y' )

proof

let s2 be Element of RAT+ ; :: thesis: ( s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) iff s2 < x' + y' )
thus ( s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) implies s2 < x' + y' ) :: thesis: ( s2 < x' + y' implies s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) )

proof

assume s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) ; :: thesis: s2 < x' + y'
then consider r1, s1 being Element of RAT+ such that
A12: s2 = r1 + s1 and
A13: r1 in DEDEKIND_CUT x and
A14: s1 in DEDEKIND_CUT y ;
ex s being Element of RAT+ st
( s = s1 & s < y' ) by A10, A14;
then A15: x' + s1 < x' + y' by ARYTM_3:83;
ex s being Element of RAT+ st
( s = r1 & s < x' ) by A8, A13;
then r1 + s1 <=' x' + s1 by ARYTM_3:83;
hence s2 < x' + y' by A12, A15, ARYTM_3:76; :: thesis: verum

end;

assume s2 < x' + y' ; :: thesis: s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y)
then consider t2, t0 being Element of RAT+ such that
A16: s2 = t2 + t0 and
A17: t2 < x' and
A18: t0 < y' by A5, A6, A7, A9, Lm46;
A19: t0 in DEDEKIND_CUT y by A10, A18;
t2 in DEDEKIND_CUT x by A8, A17;
hence s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) by A16, A19; :: thesis: verum

end;

then consider r being Element of RAT+ such that
A20: GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) = r and
A21: for s being Element of RAT+ holds
( s in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) iff s < r ) by Def4;
A22: for s being Element of RAT+ holds
( s < x' + y' iff s < r )

proof

let s be Element of RAT+ ; :: thesis: ( s < x' + y' iff s < r )
( s in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) iff s < x' + y' ) by A11;
hence ( s < x' + y' iff s < r ) by A21; :: thesis: verum

end;

thus x + y = GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) by A5, A6, Def8
.= x' + y' by A20, A22, Lm6 ; :: thesis: verum

end;

end;