take R ; :: thesis: R is R -monomorphic
take id R ; :: according to RING_3:def 3 :: thesis: ( id R is RingHomomorphism & id R is monomorphism )
thus ( id R is RingHomomorphism & id R is monomorphism ) ; :: thesis: verum