let r, s be Element of RAT+ ; :: thesis: ( r < s implies ex t being Element of RAT+ st
( r < t & t < s ) )
assume A1: r < s ; :: thesis: ex t being Element of RAT+ st
( r < t & t < s )
then consider x being Element of RAT+ such that
A2: s = r + x by Def13;
consider y being Element of RAT+ such that
A3: x = y + y by Th60;
take t = r + y; :: thesis: ( r < t & t < s )
A4: s = t + y by A2, A3, Th51;
then A5: t <=' s ;
r <=' t ;
hence r < t by A1, A4, Th66; :: thesis: t < s
r <> s by A1;
then s <> t by A4, Th62;
hence t < s by A5, Th66; :: thesis: verum