now :: thesis: for x, y being object st [x,y] in B |` R holds
[x,y] in [:X,Y:]
let x, y be object ; :: thesis: ( [x,y] in B |` R implies [x,y] in [:X,Y:] )
assume [x,y] in B |` R ; :: thesis: [x,y] in [:X,Y:]
then [x,y] in R by RELAT_1:def 12;
hence [x,y] in [:X,Y:] ; :: thesis: verum
end;
hence B |` R is Relation of X,Y by RELAT_1:def 3; :: thesis: verum