:: deftheorem Def4 defines gr GROUP_4:def 4 :
for G being Group
for A being Subset of G
for b₃ being strict Subgroup of G holds
( b₃ = gr A iff ( A c= the carrier of b₃ & ( for H being strict Subgroup of G st A c= the carrier of H holds
b₃ is Subgroup of H ) ) );