let A be Ordinal; :: thesis: 1,A are_relative_prime
let c, d1, d2 be Ordinal; :: according to ARYTM_3:def 2 :: thesis: ( 1 = c *^ d1 & A = c *^ d2 implies c = 1 )
thus ( 1 = c *^ d1 & A = c *^ d2 implies c = 1 ) by ORDINAL3:37; :: thesis: verum