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