:: deftheorem Def10 defines center GROUP_5:def 10 :
for G being Group
for b₂ being strict Subgroup of G holds
( b₂ = center G iff the carrier of b₂ = { a where a is Element of G : for b being Element of G holds a * b = b * a } );