let x9, y9, z9 be Element of RAT+ ; :: thesis: ( z9 < x9 + y9 & x9 <> {} & y9 <> {} implies ex r, s being Element of RAT+ st
( z9 = r + s & r < x9 & s < y9 ) )
assume that
A1: z9 < x9 + y9 and
A2: x9 <> {} and
A3: y9 <> {} ; :: thesis: ex r, s being Element of RAT+ st
( z9 = r + s & r < x9 & s < y9 )
consider r0, t0 being Element of RAT+ such that
A4: z9 = r0 + t0 and
A5: r0 <=' x9 and
A6: ( t0 <=' y9 & t0 <> y9 ) by A1, A3, ARYTM_3:90;
per cases ( r0 = {} or r0 <> {} ) ;
suppose A7: r0 = {} ; :: thesis: ex r, s being Element of RAT+ st
( z9 = r + s & r < x9 & s < y9 )
take {} ; :: thesis: ex s being Element of RAT+ st
( z9 = {} + s & {} < x9 & s < y9 )
take t0 ; :: thesis: ( z9 = {} + t0 & {} < x9 & t0 < y9 )
thus z9 = {} + t0 by A4, A7; :: thesis: ( {} < x9 & t0 < y9 )
{} <=' x9 by ARYTM_3:64;
hence {} < x9 by A2, ARYTM_3:68; :: thesis: t0 < y9
thus t0 < y9 by A6, ARYTM_3:68; :: thesis: verum
end;
suppose A8: r0 <> {} ; :: thesis: ex r, s being Element of RAT+ st
( z9 = r + s & r < x9 & s < y9 )
t0 < y9 by A6, ARYTM_3:68;
then consider t1 being Element of RAT+ such that
A9: t0 < t1 and
A10: t1 < y9 by ARYTM_3:93;
z9 < t1 + r0 by A4, A9, ARYTM_3:76;
then consider t2, r1 being Element of RAT+ such that
A11: z9 = t2 + r1 and
A12: t2 <=' t1 and
A13: ( r1 <=' r0 & r1 <> r0 ) by A8, ARYTM_3:90;
take r1 ; :: thesis: ex s being Element of RAT+ st
( z9 = r1 + s & r1 < x9 & s < y9 )
take t2 ; :: thesis: ( z9 = r1 + t2 & r1 < x9 & t2 < y9 )
thus z9 = r1 + t2 by A11; :: thesis: ( r1 < x9 & t2 < y9 )
r1 < r0 by A13, ARYTM_3:68;
hence r1 < x9 by A5, ARYTM_3:69; :: thesis: t2 < y9
thus t2 < y9 by A10, A12, ARYTM_3:69; :: thesis: verum
end;
end;