theorem Th18: :: GRNILP_1:18

for G being Group
for F being FinSequence of the_normal_subgroups_of G holds F is FinSequence of Subgroups G