set x = the Element of L;

take uparrow the Element of L ; :: thesis: ( not uparrow the Element of L is empty & uparrow the Element of L is upper & uparrow the Element of L is filtered )

thus ( not uparrow the Element of L is empty & uparrow the Element of L is upper & uparrow the Element of L is filtered ) ; :: thesis: verum

take uparrow the Element of L ; :: thesis: ( not uparrow the Element of L is empty & uparrow the Element of L is upper & uparrow the Element of L is filtered )

thus ( not uparrow the Element of L is empty & uparrow the Element of L is upper & uparrow the Element of L is filtered ) ; :: thesis: verum