set x = the Element of L;
take downarrow the Element of L ; :: thesis: downarrow the Element of L is principal
thus downarrow the Element of L is principal by WAYBEL_0:48; :: thesis: verum