let a, b be natural Ordinal; :: thesis: ( a,b are_relative_prime iff a hcf b = 1 )
( a hcf b divides a & a hcf b divides b ) by Def5;
then ( a = (a hcf b) *^ (a div^ (a hcf b)) & b = (a hcf b) *^ (b div^ (a hcf b)) ) by Th11;
hence ( a,b are_relative_prime implies a hcf b = 1 ) by Def2; :: thesis: ( a hcf b = 1 implies a,b are_relative_prime )
assume A1: a hcf b = 1 ; :: thesis: a,b are_relative_prime
let c, d1, d2 be Ordinal; :: according to ARYTM_3:def 2 :: thesis: ( a = c *^ d1 & b = c *^ d2 implies c = 1 )
assume A2: ( a = c *^ d1 & b = c *^ d2 ) ; :: thesis: c = 1
( a <> {} or b <> {} ) by A1, Th19;
then reconsider c = c as Element of omega by A2, ORDINAL3:88;
( c divides a & c divides b ) by A2, Def3;
then c divides 1 by A1, Def5;
then ex d being natural Ordinal st 1 = c *^ d by Th9;
hence c = 1 by ORDINAL3:41; :: thesis: verum