not [0,0] in RAT+
proof
assume A1: [0,0] in RAT+ ; :: thesis: contradiction
reconsider i = 0 as Element of omega by ORDINAL1:def 12;
( i,i are_coprime & i <> {} & i <> 1 ) by A1, ARYTM_3:33;
hence contradiction ; :: thesis: verum
end;
hence RAT+ c= RAT by XBOOLE_1:7, ZFMISC_1:34, NUMBERS:def 3; :: thesis: verum