:: deftheorem Def5 defines Subgroup GROUP_2:def 5 :
for G, b₂ being non empty Group-like multMagma holds
( b₂ is Subgroup of G iff ( the carrier of b₂ c= the carrier of G & the multF of b₂ = the multF of G || the carrier of b₂ ) );