let z', x', y' be Element of RAT+ ; :: thesis: ( z' < x' + y' & x' <> {} & y' <> {} implies ex r, s being Element of RAT+ st
( z' = r + s & r < x' & s < y' ) )
assume that
A1: z' < x' + y' and
A2: x' <> {} and
A3: y' <> {} ; :: thesis: ex r, s being Element of RAT+ st
( z' = r + s & r < x' & s < y' )
consider r0, t0 being Element of RAT+ such that
A4: z' = r0 + t0 and
A5: r0 <=' x' and
A6: ( t0 <=' y' & t0 <> y' ) by A1, A3, ARYTM_3:98;

per cases ( r0 = {} or r0 <> {} ) ;

suppose A7: r0 = {} ; :: thesis: ex r, s being Element of RAT+ st
( z' = r + s & r < x' & s < y' )

take {} ; :: thesis: ex s being Element of RAT+ st
( z' = {} + s & {} < x' & s < y' )
take t0 ; :: thesis: ( z' = {} + t0 & {} < x' & t0 < y' )
thus z' = {} + t0 by A4, A7; :: thesis: ( {} < x' & t0 < y' )
{} <=' x' by ARYTM_3:71;
hence {} < x' by A2, ARYTM_3:75; :: thesis: t0 < y'
thus t0 < y' by A6, ARYTM_3:75; :: thesis: verum

end;

suppose A8: r0 <> {} ; :: thesis: ex r, s being Element of RAT+ st
( z' = r + s & r < x' & s < y' )

t0 < y' by A6, ARYTM_3:75;
then consider t1 being Element of RAT+ such that
A9: t0 < t1 and
A10: t1 < y' by ARYTM_3:101;
z' < t1 + r0 by A4, A9, ARYTM_3:83;
then consider t2, r1 being Element of RAT+ such that
A11: z' = t2 + r1 and
A12: t2 <=' t1 and
A13: ( r1 <=' r0 & r1 <> r0 ) by A8, ARYTM_3:98;
take r1 ; :: thesis: ex s being Element of RAT+ st
( z' = r1 + s & r1 < x' & s < y' )
take t2 ; :: thesis: ( z' = r1 + t2 & r1 < x' & t2 < y' )
thus z' = r1 + t2 by A11; :: thesis: ( r1 < x' & t2 < y' )
r1 < r0 by A13, ARYTM_3:75;
hence r1 < x' by A5, ARYTM_3:76; :: thesis: t2 < y'
thus t2 < y' by A10, A12, ARYTM_3:76; :: thesis: verum

end;

end;