take R ; :: thesis: R is R -isomorphic
take id R ; :: according to RING_3:def 4 :: thesis: ( id R is RingHomomorphism & id R is isomorphism )
thus ( id R is RingHomomorphism & id R is isomorphism ) ; :: thesis: verum