1,2 are_coprime by ORDINAL3:37;
then A1: [1,2] in RAT+ by ARYTM_3:33, Lm11;
not 1 in {0} by TARSKI:def 1;
then ( not [1,2] in NAT & not [1,2] in [:{0},NAT:] ) by ARYTM_3:32, ZFMISC_1:87;
then not [1,2] in NAT \/ [:{0},NAT:] by XBOOLE_0:def 3;
then INT <> RAT by A1, Lm4, XBOOLE_0:def 5;
hence INT c< RAT by Lm15; :: thesis: verum