A1: now

let x, y be set ; :: 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 ( y in B & [x,y] in R ) by RELAT_1:def 12;
hence [x,y] in [:X,Y:] ; :: thesis: verum

end;

reconsider P = [:X,Y:] as Relation ;
B | R c= P by A1, RELAT_1:def 3;
hence B | R is Relation of X,Y by Def1; :: thesis: verum