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