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