theorem Th17: :: GRNILP_1:17

for G being Group holds the_normal_subgroups_of G c= Subgroups G