given y being set such that A1: [{} ,y] in RAT+ ; :: thesis: contradiction
consider i, j being Element of omega such that
A2: ( [{} ,y] = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 ) by Th38, Th35, A1;
i = {} by A2, ZFMISC_1:33;
hence contradiction by A2, Th7; :: thesis: verum