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