let X be set ; :: thesis: for E being non empty set
for A being non empty automaton of (Lex E) \/ {(<%> E)} st X in the FinalS of (_bool A) holds
X meets the FinalS of A
let E be non empty set ; :: thesis: for A being non empty automaton of (Lex E) \/ {(<%> E)} st X in the FinalS of (_bool A) holds
X meets the FinalS of A
let A be non empty automaton of (Lex E) \/ {(<%> E)}; :: thesis: ( X in the FinalS of (_bool A) implies X meets the FinalS of A )
assume A1: X in the FinalS of (_bool A) ; :: thesis: X meets the FinalS of A
the FinalS of (_bool A) = { Q where Q is Element of (_bool A) : Q meets the FinalS of A } by Def6;
then ex Q being Element of (_bool A) st
( X = Q & Q meets the FinalS of A ) by A1;
hence X meets the FinalS of A ; :: thesis: verum