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