take {} ; :: thesis: ( {} is X -defined & {} is Y -valued )
thus ( {} is X -defined & {} is Y -valued ) by Lm2; :: thesis: verum