:: deftheorem DefA5 defines Subgroup GROUP_1A:def 15 :
for G, b₂ being non empty addGroup-like addMagma holds
( b₂ is Subgroup of G iff ( the carrier of b₂ c= the carrier of G & the addF of b₂ = the addF of G || the carrier of b₂ ) );