set x = the Element of L;
take downarrow the Element of L ; :: thesis: ( not downarrow the Element of L is empty & downarrow the Element of L is lower & downarrow the Element of L is directed )
thus ( not downarrow the Element of L is empty & downarrow the Element of L is lower & downarrow the Element of L is directed ) ; :: thesis: verum