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