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