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

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

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

then denominator x = 1 by Def9;
hence numerator x, denominator x are_coprime by Th2; :: thesis: verum

end;

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

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

end;

end;