let E be non empty set ; :: thesis: for FA being non empty finite automaton over (Lex E) \/ {(<%> E)} ex DFA being non empty finite deterministic automaton over Lex E st Lang FA = Lang DFA
let FA be non empty finite automaton over (Lex E) \/ {(<%> E)}; :: thesis: ex DFA being non empty finite deterministic automaton over Lex E st Lang FA = Lang DFA
set bNFA = _bool FA;
Lang FA = Lang (_bool FA) by Th38;
hence ex DFA being non empty finite deterministic automaton over Lex E st Lang FA = Lang DFA ; :: thesis: verum