theorem :: RELAT_1:158

for X, Y being set holds dom [:X,Y:] c= X