for e being Element of E holds <%e%> in Lex E by FLANG_1:def 4;
hence not Lex E is empty ; :: thesis: verum