let E be non empty set ; :: thesis: not <%> E in Lex E

assume <%> E in Lex E ; :: thesis: contradiction

then ex e being Element of E st

( e in E & <%> E = <%e%> ) by FLANG_1:def 4;

hence contradiction ; :: thesis: verum

assume <%> E in Lex E ; :: thesis: contradiction

then ex e being Element of E st

( e in E & <%> E = <%e%> ) by FLANG_1:def 4;

hence contradiction ; :: thesis: verum