for IAlph being non empty set
for fsm being non empty FSM over IAlph
for q being State of fsm holds <*q*> is_admissible_for <*> IAlph