for I being non empty set
for S being non empty FSM over I
for q being State of S st q is accessible & q <> the InitS of S holds
ex s being Element of I st q is_accessible_via s