for r, s being Element of RAT+ holds
( r < s iff ( r <=' s & r <> s ) ) by Th66;