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 A: 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 defBoolA;
then consider Q being Element of (_bool A) such that
B: ( X = Q & Q meets the FinalS of A ) by A;
thus X meets the FinalS of A by B; :: thesis: verum