set x = the Element of (Image c);
take downarrow the Element of (Image c) ; :: thesis: ( not downarrow the Element of (Image c) is empty & downarrow the Element of (Image c) is directed )
thus ( not downarrow the Element of (Image c) is empty & downarrow the Element of (Image c) is directed ) ; :: thesis: verum