:: deftheorem Def17 defines Morphs RINGCAT1:def 17 :
for V being Ring_DOMAIN
for b₂ being RingMorphism_DOMAIN holds
( b₂ = Morphs V iff for x being object holds
( x in b₂ iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) );