theorem :: GROUP_9:61

for O, E being set
for A being Action of O,E holds [#] E is_stable_under_the_action_of A ;