:: deftheorem Def2 defines the_stable_subset_generated_by GROUP_9:def 2 :
for O, E being set
for A being Action of O,E
for X, b₅ being Subset of E holds
( b₅ = the_stable_subset_generated_by (X,A) iff ( X c= b₅ & b₅ is_stable_under_the_action_of A & ( for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds
b₅ c= Y ) ) );