:: deftheorem Def3 defines -monomorphic RING_3:def 3 :
for R, S being Ring holds
( S is R -monomorphic iff ex f being Function of R,S st
( f is RingHomomorphism & f is monomorphism ) );