let A be Ordinal; :: thesis: ( {} ,A are_relative_prime implies A = 1 )
A1: ( {} = A *^ {} & A = A *^ 1 ) by ORDINAL2:38, ORDINAL2:39;
assume ( {} ,A are_relative_prime & A <> 1 ) ; :: thesis: contradiction
hence contradiction by A1, Def2; :: thesis: verum