let x be Element of RAT+ ; :: thesis: ( x <> {} implies ex y being Element of RAT+ st x *' y = 1 )
set nx = numerator x;
set dx = denominator x;
assume x <> {} ; :: thesis: ex y being Element of RAT+ st x *' y = 1
then A1: ( numerator x <> {} & denominator x <> {} ) by Th41, Th43;
take y = (denominator x) / (numerator x); :: thesis: x *' y = 1
numerator x, denominator x are_relative_prime by Th40;
then ( denominator y = numerator x & numerator y = denominator x ) by A1, Th49;
hence x *' y = 1 by A1, Th47, ORDINAL3:34; :: thesis: verum