:: deftheorem Def26 defines the_stable_subgroup_of GROUP_9:def 26 :
for O being set
for G being GroupWithOperators of O
for A being Subset of G
for b₄ being strict StableSubgroup of G holds
( b₄ = the_stable_subgroup_of A iff ( A c= the carrier of b₄ & ( for H being strict StableSubgroup of G st A c= the carrier of H holds
b₄ is StableSubgroup of H ) ) );