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