set m = tfsm;
set AS = { q where q is State of tfsm : q is accessible } ;
A1: { 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 ex q being State of tfsm st
( x = q & q is accessible ) ;
hence x in the carrier of tfsm ; :: thesis: verum

end;

the InitS of tfsm, <*> IAlph -leads_to the InitS of tfsm by Th17;
then the InitS of tfsm is accessible by Def21;
then the InitS of tfsm in { q where q is State of tfsm : q is accessible } ;
hence ( accessibleStates tfsm is finite & not accessibleStates tfsm is empty ) by A1; :: thesis: verum