let x be Element of RAT+ ; :: thesis: ( x <> {} iff numerator x <> {} )

hereby :: thesis: ( numerator x <> {} implies x <> {} )

assume A1: ( x <> {} & numerator x = {} ) ; :: thesis: contradiction
then A2: not x in omega by Def8;
then consider i, j being Element of omega such that
A3: ( x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 ) by Th35;
i = {} by A1, A2, A3, Def8;
hence contradiction by A3, Th7; :: thesis: verum

end;

{} in omega by ORDINAL1:def 12;
hence ( numerator x <> {} implies x <> {} ) by Def8; :: thesis: verum