take X --> the Element of Y ; :: thesis: X --> the Element of Y is constant
thus X --> the Element of Y is constant ; :: thesis: verum