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