let x be Element of RAT+ ; ( x <> {} iff numerator x <> {} )
hereby ( numerator x <> {} implies x <> {} )
assume that A1:
x <> {}
and A2:
numerator x = {}
;
contradictionA3:
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;
verum
end;
{} in omega
by ORDINAL1:def 11;
hence
( numerator x <> {} implies x <> {} )
by Def8; verum