consider x being Element of X;
reconsider x9 = x as Element of L ;
x9 <= x9 ;
hence not downarrow X is empty by Def15; :: thesis: verum