let E be non empty set ; :: thesis: for A being non empty automaton over (Lex E) \/ {(<%> E)} ex DA being non empty deterministic automaton over Lex E st Lang A = Lang DA
let A be non empty automaton over (Lex E) \/ {(<%> E)}; :: thesis: ex DA being non empty deterministic automaton over Lex E st Lang A = Lang DA
set DA = _bool A;
take _bool A ; :: thesis: Lang A = Lang (_bool A)
thus Lang A = Lang (_bool A) by Th38; :: thesis: verum