let r, s, t be Element of RAT+ ; :: thesis: ( r <=' s + t implies ex s0, t0 being Element of RAT+ st
( r = s0 + t0 & s0 <=' s & t0 <=' t ) )
assume A1: r <=' s + t ; :: thesis: ex s0, t0 being Element of RAT+ st
( r = s0 + t0 & s0 <=' s & t0 <=' t )

per cases ( s <=' r or r <=' s ) ;

suppose s <=' r ; :: thesis: ex s0, t0 being Element of RAT+ st
( r = s0 + t0 & s0 <=' s & t0 <=' t )

then ( s <=' s & ex t0 being Element of RAT+ st
( r = s + t0 & t0 <=' t ) ) by A1, Th86;
hence ex s0, t0 being Element of RAT+ st
( r = s0 + t0 & s0 <=' s & t0 <=' t ) ; :: thesis: verum

end;

suppose A2: r <=' s ; :: thesis: ex s0, t0 being Element of RAT+ st
( r = s0 + t0 & s0 <=' s & t0 <=' t )

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

end;

end;