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 Th41;
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, Th45;
then ((numerator r) *^ (numerator s)) *^ 1 = ((denominator r) *^ (denominator s)) *^ {} by A2, Th51
.= {} by ORDINAL2:35 ;
then (numerator r) *^ (numerator s) = {} by ORDINAL3:31;
then ( numerator r = {} or numerator s = {} ) by ORDINAL3:31;
hence ( r = {} or s = {} ) by Th43; :: thesis: verum