let r, s be Element of RAT+ ; :: thesis: ( not r *' s = {} or r = {} or s = {} )
set nr = numerator r;
set dr = denominator r;
set ns = numerator s;
set ds = denominator s;
assume A1: r *' s = {} ; :: thesis: ( r = {} or s = {} )
( denominator r <> {} & denominator s <> {} ) by Th35;
then A2: (denominator r) *^ (denominator s) <> {} by ORDINAL3:31;
( denominator {} = 1 & numerator {} = {} ) by Def8, Def9, Lm1;
then ((numerator r) *^ (numerator s)) / ((denominator r) *^ (denominator s)) = {} / 1 by A1, Th39;
then ((numerator r) *^ (numerator s)) *^ 1 = ((denominator r) *^ (denominator s)) *^ {} by A2, Th45, Lm4
.= {} by ORDINAL2:35 ;
then (numerator r) *^ (numerator s) = {} by ORDINAL3:31, Lm4;
then ( numerator r = {} or numerator s = {} ) by ORDINAL3:31;
hence ( r = {} or s = {} ) by Th37; :: thesis: verum