:: deftheorem defines leads_to_final_state_of FSM_2:def 5 :
for I being non empty set
for s being Element of I
for S being non empty SM_Final over I holds
( s leads_to_final_state_of S iff ex q being State of S st
( q is_accessible_via s & q in the FinalS of S ) );