now

let x, y be set ; :: thesis: ( [x,y] in R | A implies [x,y] in [:X,Y:] )
assume [x,y] in R | A ; :: thesis: [x,y] in [:X,Y:]
then ( x in A & [x,y] in R ) by RELAT_1:def 11;
hence [x,y] in [:X,Y:] ; :: thesis: verum

end;

hence R | A is Relation of X,Y by RELAT_1:def 3; :: thesis: verum