let IAlph, OAlph be non empty set ; :: thesis: 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 ) ) )
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis: ( accessibleStates tfsm c= the carrier of tfsm & ( for q being State of tfsm holds
( q in accessibleStates tfsm iff q is accessible ) ) )
set AS = { q where q is State of tfsm : q is accessible } ;
{ q where q is State of tfsm : q is accessible } c= the carrier of tfsm

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is State of tfsm : q is accessible } or x in the carrier of tfsm )
assume x in { q where q is State of tfsm : q is accessible } ; :: thesis: x in the carrier of tfsm
then ex q being State of tfsm st
( x = q & q is accessible ) ;
hence x in the carrier of tfsm ; :: thesis: verum

end;

hence accessibleStates tfsm c= the carrier of tfsm ; :: thesis: for q being State of tfsm holds
( q in accessibleStates tfsm iff q is accessible )
let q be State of tfsm; :: thesis: ( q in accessibleStates tfsm iff q is accessible )

hereby :: thesis: ( q is accessible implies q in accessibleStates tfsm )

assume q in accessibleStates tfsm ; :: thesis: q is accessible
then ex q9 being State of tfsm st
( q9 = q & q9 is accessible ) ;
hence q is accessible ; :: thesis: verum

end;

thus ( q is accessible implies q in accessibleStates tfsm ) ; :: thesis: verum