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

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