:: deftheorem Def2 defines -Subgroup-yielding GROUP_23:def 2 :
for I being set
for F, IT being Group-Family of I holds
( IT is F -Subgroup-yielding iff for i being Element of I
for G being Group st G = F . i holds
IT . i is Subgroup of G );