reconsider SA = semiautomaton(# the carrier of A,the Tran of A,the InitS of A #) as non empty semiautomaton of F ;
set cA = the carrier of (_bool SA);
reconsider tA = the Tran of (_bool SA) as Relation of , ;
set iA = the InitS of (_bool SA);
{ Q where Q is Element of : Q meets the FinalS of A } is Subset of

proof

defpred S₁[ set ] means $1 meets the FinalS of A;
{ Q where Q is Element of : S₁[Q] } c= the carrier of (_bool SA) from FRAENKEL:sch 10();
hence { Q where Q is Element of : Q meets the FinalS of A } is Subset of ; :: thesis: verum

end;

then reconsider fA = { Q where Q is Element of : Q meets the FinalS of A } as Subset of ;
set bA = automaton(# the carrier of (_bool SA),tA,the InitS of (_bool SA),fA #);
reconsider bA = automaton(# the carrier of (_bool SA),tA,the InitS of (_bool SA),fA #) as non empty strict deterministic automaton of Lex E by Def5;
take bA ; :: thesis: ( semiautomaton(# the carrier of bA,the Tran of bA,the InitS of bA #) = _bool semiautomaton(# the carrier of A,the Tran of A,the InitS of A #) & the FinalS of bA = { Q where Q is Element of : Q meets the FinalS of A } )
thus ( semiautomaton(# the carrier of bA,the Tran of bA,the InitS of bA #) = _bool semiautomaton(# the carrier of A,the Tran of A,the InitS of A #) & the FinalS of bA = { Q where Q is Element of : Q meets the FinalS of A } ) ; :: thesis: verum