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