:: deftheorem Def2 defines ProjGroup GROUP_12:def 2 :
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for b₄ being strict Subgroup of product F holds
( b₄ = ProjGroup (F,i) iff the carrier of b₄ = ProjSet (F,i) );