theorem ThS2: :: GROUP_23:70

for I being non empty set
for G being Group
for F being Subgroup-Family of I,G holds
( F is componentwise_strict iff for i being Element of I holds F . i is strict Subgroup of G ) ;