:: deftheorem Def6 defines SubAbGr RING_EMB:def 6 :
for G, b₂ being AbGroup holds
( b₂ is SubAbGr of G iff ( the carrier of b₂ c= the carrier of G & the addF of b₂ = the addF of G || the carrier of b₂ & 0. b₂ = 0. G ) );