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

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

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

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

end;

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

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

end;

suppose A5: ( y <> {} & x <> {} ) ; :: thesis: ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x + y = x9 + y9 )

set A = DEDEKIND_CUT x;
set B = DEDEKIND_CUT y;
consider x9 being Element of RAT+ such that
A6: x = x9 and
A7: DEDEKIND_CUT x = { s where s is Element of RAT+ : s < x9 } by A1, Def3;
consider y9 being Element of RAT+ such that
A8: y = y9 and
A9: DEDEKIND_CUT y = { s where s is Element of RAT+ : s < y9 } by A2, Def3;
A10: for s being Element of RAT+ holds
( s in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) iff s < x9 + y9 )

proof

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

proof

assume s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) ; :: thesis: s2 < x9 + y9
then consider r1, s1 being Element of RAT+ such that
A11: s2 = r1 + s1 and
A12: r1 in DEDEKIND_CUT x and
A13: s1 in DEDEKIND_CUT y ;
ex s being Element of RAT+ st
( s = r1 & s < x9 ) by A7, A12;
then A14: r1 + s1 <=' x9 + s1 by ARYTM_3:76;
ex s being Element of RAT+ st
( s = s1 & s < y9 ) by A9, A13;
then x9 + s1 < x9 + y9 by ARYTM_3:76;
hence s2 < x9 + y9 by A11, A14, ARYTM_3:69; :: thesis: verum

end;

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

end;

then consider r being Element of RAT+ such that
A17: GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) = r and
A18: for s being Element of RAT+ holds
( s in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) iff s < r ) by Def4;
A19: for s being Element of RAT+ holds
( s < x9 + y9 iff s < r ) by A10, A18;
take x9 ; :: thesis: ex y9 being Element of RAT+ st
( x = x9 & y = y9 & x + y = x9 + y9 )
take y9 ; :: thesis: ( x = x9 & y = y9 & x + y = x9 + y9 )
thus ( x = x9 & y = y9 ) by A6, A8; :: thesis: x + y = x9 + y9
thus x + y = GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) by A5, Def8
.= x9 + y9 by A17, A19, Lm6 ; :: thesis: verum

end;

end;