:: deftheorem defines is_stable_under_the_action_of GROUP_9:def 1 :
for O, E being set
for A being Action of O,E
for IT being set holds
( IT is_stable_under_the_action_of A iff for o being Element of O
for f being Function of E,E st o in O & f = A . o holds
f .: IT c= IT );