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