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

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