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 [:the carrier of (_bool SA),(Lex E):],the carrier of (_bool SA) ;
set iA = the InitS of (_bool SA);
{ Q where Q is Element of (_bool SA) : Q meets the FinalS of A } is Subset of the carrier of (_bool SA)

proof

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

end;

then reconsider fA = { Q where Q is Element of (_bool SA) : Q meets the FinalS of A } as Subset of the carrier of (_bool SA) ;
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 bA : 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 bA : Q meets the FinalS of A } ) ; :: thesis: verum