take X --> the Element of Y ; :: thesis: ( not X --> the Element of Y is empty & X --> the Element of Y is X -defined & X --> the Element of Y is Y -valued )
thus ( not X --> the Element of Y is empty & X --> the Element of Y is X -defined & X --> the Element of Y is Y -valued ) ; :: thesis: verum