let x be Element of RAT+ ; :: thesis: (numerator x) / (denominator x) = x
A1: denominator x <> {} by Th41;
A2: RED ((numerator x),(denominator x)) = numerator x by Th28, Th40;
numerator x, denominator x are_relative_prime by Th40;
then A3: RED ((denominator x),(numerator x)) = denominator x by Th28;

per cases ( denominator x = 1 or denominator x <> 1 ) ;

suppose A4: denominator x = 1 ; :: thesis: (numerator x) / (denominator x) = x

then x in omega by Th42;
then numerator x = x by Def8;
hence (numerator x) / (denominator x) = x by A2, A3, A4, Def10; :: thesis: verum

end;

suppose A5: denominator x <> 1 ; :: thesis: (numerator x) / (denominator x) = x

then not x in omega by Def9;
then x = [(numerator x),(denominator x)] by Th42;
hence (numerator x) / (denominator x) = x by A1, A2, A3, A5, Def10; :: thesis: verum

end;

end;