let A be Ordinal; :: thesis: ( {} ,A are_relative_prime implies A = 1 )
assume A1: ( {} ,A are_relative_prime & A <> 1 ) ; :: thesis: contradiction
then ( A in 1 or 1 in A ) by ORDINAL1:24;
then ( 1 in A & {} = A *^ {} & A = A *^ 1 ) by A1, Th5, ORDINAL2:55, ORDINAL2:56, ORDINAL3:17;
hence contradiction by A1, Def2; :: thesis: verum