let x be Element of RAT+ ; :: thesis: numerator x, denominator x are_relative_prime

per cases ( x in omega or not x in omega ) ;

suppose x in omega ; :: thesis: numerator x, denominator x are_relative_prime

then denominator x = 1 by Def9;
hence numerator x, denominator x are_relative_prime by Th6; :: thesis: verum

end;

suppose A1: not x in omega ; :: thesis: numerator x, denominator x are_relative_prime

then consider i, j being Element of omega such that
A2: x = [i,j] and
A3: i,j are_relative_prime and
j <> {} and
j <> 1 by Th35;
i = numerator x by A1, A2, Def8;
hence numerator x, denominator x are_relative_prime by A1, A2, A3, Def9; :: thesis: verum

end;

end;