let r, s, t be Element of RAT+ ; :: thesis:
assume that
A1: s < r + t and
A2: t <> {} ; :: thesis:

per cases ;

suppose r <=' s ; :: thesis:

then consider t0 being Element of RAT+ such that
A3: ( s = r + t0 & t0 <=' t ) by A1, Th86;
take r ; :: thesis:
take t0 ; :: thesis:
thus ( s = r + t0 & r <=' r & t0 <=' t & t0 <> t ) by A1, A3; :: thesis:

end;

suppose A4: s <=' r ; :: thesis:

( s = s + {} & {} <=' t ) by Th50, Th64;
hence ex r0, t0 being Element of RAT+ st
( s = r0 + t0 & r0 <=' r & t0 <=' t & t0 <> t ) by A2, A4; :: thesis:

end;

end;