let r1, r2, s1, s2 be Element of RAT+ ; ( not r1 *' r2 = s1 *' s2 or r1 <=' s1 or r2 <=' s2 )
assume A1:
r1 *' r2 = s1 *' s2
; ( r1 <=' s1 or r2 <=' s2 )
A2:
{} <=' s1
by Th64;
assume that
A3:
s1 < r1
and
A4:
s2 < r2
; 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; verum