:: deftheorem Def10 defines the_strict_stabilizer_of GROUP_10:def 10 :
for G being Group
for E being non empty set
for T being LeftOperation of G,E
for A being Subset of E
for b₅ being strict Subgroup of G holds
( b₅ = the_strict_stabilizer_of (A,T) iff the carrier of b₅ = { g where g is Element of G : (T ^ g) .: A = A } );