take R ; :: thesis: ( R is R -homomorphic & R is R -monomorphic )
id R is RingHomomorphism ;
hence R is R -homomorphic ; :: thesis: R is R -monomorphic
id R is RingMonomorphism ;
hence R is R -monomorphic by RING_3:def 3; :: thesis: verum