consider x being Element of L;
take downarrow x ; :: thesis: ( not downarrow x is empty & downarrow x is lower & downarrow x is directed )
thus ( not downarrow x is empty & downarrow x is lower & downarrow x is directed ) ; :: thesis: verum