let r1, r2, s1, s2 be Element of RAT+ ; :: thesis: ( not r1 *' r2 = s1 *' s2 or r1 <=' s1 or r2 <=' s2 )
assume A1: r1 *' r2 = s1 *' s2 ; :: thesis: ( r1 <=' s1 or r2 <=' s2 )
A2: {} <=' s1 by Th64;
assume that
A3: s1 < r1 and
A4: s2 < r2 ; :: thesis: contradiction
( s2 <> r2 & s1 *' s2 <=' r1 *' s2 ) by A3, A4, Th82;
then s1 *' s2 < r1 *' s2 by A1, A3, A2, Th56, Th66;
hence contradiction by A1, A4, Th82; :: thesis: verum