:: deftheorem Def7 defines StableSubgroup GROUP_9:def 7 :
for O being set
for G being GroupWithOperators of O
for b₃ being non empty Group-like associative distributive HGrWOpStr over O holds
( b₃ is StableSubgroup of G iff ( b₃ is Subgroup of G & ( for o being Element of O holds b₃ ^ o = (G ^ o) | the carrier of b₃ ) ) );