:: deftheorem Def5 defines leads_to_under FSM_1:def 5 :
for IAlph being non empty set
for fsm being non empty FSM over IAlph
for q being State of fsm
for w being FinSequence of IAlph
for b₅ being State of fsm holds
( b₅ = q leads_to_under w iff q,w -leads_to b₅ );