given y being object 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_coprime and
j <> {} and
A4: j <> 1 by A1, Th29, Th32;
i = {} by A2, XTUPLE_0:1;
hence contradiction by A3, A4, Th3; :: thesis: verum