let E be non empty set ; :: thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds _bool TS is non empty transition-system over (Lex E) \/ {(<%> E)}
let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; :: thesis: _bool TS is non empty transition-system over (Lex E) \/ {(<%> E)}
Lex E c= (Lex E) \/ {(<%> E)} by XBOOLE_1:7;
then ( dom the Tran of (_bool TS) c= [: the carrier of (_bool TS),(Lex E):] & [: the carrier of (_bool TS),(Lex E):] c= [: the carrier of (_bool TS),((Lex E) \/ {(<%> E)}):] ) by ZFMISC_1:95;
hence _bool TS is non empty transition-system over (Lex E) \/ {(<%> E)} by RELSET_1:5, XBOOLE_1:1; :: thesis: verum