theorem Th29: :: ARYTM_3:29

for x being Element of RAT+ holds
( x in omega or ex i, j being Element of omega st
( x = [i,j] & i,j are_coprime & j <> {} & j <> 1 ) )