take Z = bool [:X,Y:]; :: thesis: for b₁ being X -defined Y -valued Relation holds b₁ in Z
let R be X -defined Y -valued Relation; :: thesis: R in Z
R c= [:X,Y:] by T;
hence R in Z by ZFMISC_1:def 1; :: thesis: verum