let OAlph, IAlph be non empty set ; :: thesis: for tfsm being non empty finite Mealy-FSM of 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 of 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 set ; :: 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 consider q being State of tfsm such that
A1: ( x = q & q is accessible ) ;
thus x in the carrier of tfsm by A1; :: 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 consider q' being State of tfsm such that
A2: ( q' = q & q' is accessible ) ;
thus q is accessible by A2; :: thesis: verum

end;

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