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; verum