theorem :: RELAT_1:171

for X, Y being set holds
( {} is X -defined & {} is Y -valued ) by Lm1;