let R be Ring; :: thesis: R24(R,R)
id R is isomorphism ;
hence R,R are_isomorphic ; :: thesis: verum