theorem :: GROUP_23:15

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