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;
A1: denominator x <> {} by Th35;
assume x <> {} ; :: thesis: ex y being Element of RAT+ st x *' y = 1
then A2: numerator x <> {} by Th37;
take y = (denominator x) / (numerator x); :: thesis: x *' y = 1
numerator x, denominator x are_coprime by Th34;
then ( denominator y = numerator x & numerator y = denominator x ) by A2, Th43;
hence x *' y = 1 by A2, A1, Th41, ORDINAL3:31; :: thesis: verum