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