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