let x, y be Element of RAT+ ; :: thesis: ( ( for z being Element of RAT+ holds not y = x + z ) implies ex z being Element of RAT+ st x = y + z )
set nx = numerator x;
set ny = numerator y;
set dx = denominator x;
set dy = denominator y;
A1: ( denominator x <> {} & denominator y <> {} ) by Th35;
A2: ( (numerator x) / (denominator x) = x & (numerator y) / (denominator y) = y ) by Th39;
( (numerator x) *^ (denominator y) c= (numerator y) *^ (denominator x) or (numerator y) *^ (denominator x) c= (numerator x) *^ (denominator y) ) ;
then A3: ( (numerator y) *^ (denominator x) = ((numerator x) *^ (denominator y)) +^ (((numerator y) *^ (denominator x)) -^ ((numerator x) *^ (denominator y))) or (numerator x) *^ (denominator y) = ((numerator y) *^ (denominator x)) +^ (((numerator x) *^ (denominator y)) -^ ((numerator y) *^ (denominator x))) ) by ORDINAL3:def 5;
( ((numerator x) *^ (denominator y)) / ((denominator x) *^ (denominator y)) = (numerator x) / (denominator x) & ((numerator y) *^ (denominator x)) / ((denominator x) *^ (denominator y)) = (numerator y) / (denominator y) ) by Th35, Th44;
then ( x = y + ((((numerator x) *^ (denominator y)) -^ ((numerator y) *^ (denominator x))) / ((denominator x) *^ (denominator y))) or y = x + ((((numerator y) *^ (denominator x)) -^ ((numerator x) *^ (denominator y))) / ((denominator x) *^ (denominator y))) ) by A1, A2, A3, Th47, ORDINAL3:31;
hence ( ( for z being Element of RAT+ holds not y = x + z ) implies ex z being Element of RAT+ st x = y + z ) ; :: thesis: verum