:: deftheorem Def1 defines Subgroups GROUP_3:def 1 :
for G being Group
for b₂ being set holds
( b₂ = Subgroups G iff for x being object holds
( x in b₂ iff x is strict Subgroup of G ) );