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