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