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