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

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

assume that
A1: x <> {} and
A2: numerator x = {} ; :: thesis: contradiction
A3: not x in omega by A1, A2, Def8;
then consider i, j being Element of omega such that
A4: x = [i,j] and
A5: i,j are_coprime and
j <> {} and
A6: j <> 1 by Th29;
i = {} by A2, A3, A4, Def8;
hence contradiction by A5, A6, Th3; :: thesis: verum

end;

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