:: deftheorem Def1 defines Subgroup-Family GROUP_20:def 1 :
for I being set
for G being Group
for b₃ being Group-Family of I holds
( b₃ is Subgroup-Family of I,G iff for i being object st i in I holds
b₃ . i is Subgroup of G );