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] and
A3: i,j are_relative_prime and
j <> {} and
A4: j <> 1 by A1, Th35, Th38;
i = {} by A2, ZFMISC_1:27;
hence contradiction by A3, A4, Th7; :: thesis: verum