1,2 are_relative_prime

proof

let c, d1, d2 be Ordinal; :: according to ARYTM_3:def 2 :: thesis: ( not 1 = c *^ d1 or not 2 = c *^ d2 or c = 1 )
assume that
A1: 1 = c *^ d1 and
2 = c *^ d2 ; :: thesis: c = 1
thus c = 1 by A1, ORDINAL3:37; :: thesis: verum

end;

then A2: [1,2] in RAT+ by ARYTM_3:33;
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 A2, Lm4, XBOOLE_0:def 5;
hence INT c< RAT by Lm15, XBOOLE_0:def 8; :: thesis: verum