let x be Element of RAT+ ; ( not x in omega implies ( x = [(numerator x),(denominator x)] & denominator x <> 1 ) )
assume A1:
not x in omega
; ( x = [(numerator x),(denominator x)] & denominator x <> 1 )
then consider i, j being Element of omega such that
A2:
x = [i,j]
and
i,j are_coprime
and
j <> {}
and
A3:
j <> 1
by Th29;
i = numerator x
by A1, A2, Def8;
hence
( x = [(numerator x),(denominator x)] & denominator x <> 1 )
by A1, A2, A3, Def9; verum