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 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;
the InitS of tfsm, <*> IAlph -leads_to the InitS of tfsm by Th2;
then the InitS of tfsm is accessible ;
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