let E be non empty set ; :: thesis: for TS being transition-system of Lex E holds not <%> E in rng (dom the Tran of TS)
let TS be transition-system of Lex E; :: thesis: not <%> E in rng (dom the Tran of TS)
dom the Tran of TS c= [:the carrier of TS,(Lex E):] by RELAT_1:def 18;
then rng (dom the Tran of TS) c= Lex E by RELAT_1:def 19;
hence not <%> E in rng (dom the Tran of TS) by ThLex10; :: thesis: verum