consider x being Element of L;
take downarrow x ; :: thesis: downarrow x is principal
thus downarrow x is principal by WAYBEL_0:48; :: thesis: verum