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