:: deftheorem Def20 defines /. GROUP_23:def 21 :
for G being Group
for I being set
for F being Subgroup-Family of I,G
for i being object st i in I holds
F /. i = F . i;