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