for X being set
for E being non empty set
for A being non empty automaton over (Lex E) \/ {(<%> E)} st X in the FinalS of (_bool A) holds
X meets the FinalS of A