theorem :: ARYTM_3:70

for r, s, t being Element of RAT+ st r < s & s < t holds
r < t by Th67;