for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph holds
( accessibleStates tfsm c= the carrier of tfsm & ( for q being State of tfsm holds
( q in accessibleStates tfsm iff q is accessible ) ) )