:: deftheorem defines <= RINGCAT1:def 7 :
for G, H being Ring holds
( G <= H iff ex F being RingMorphism st
( dom F = G & cod F = H ) );