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