now :: thesis: for x, y being object st [x,y] in R | A holds

[x,y] in [:X,Y:]

hence
R | A is Relation of X,Y
by RELAT_1:def 3; :: thesis: verum[x,y] in [:X,Y:]

let x, y be object ; :: 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,y] in R by RELAT_1:def 11;

hence [x,y] in [:X,Y:] ; :: thesis: verum

end;assume [x,y] in R | A ; :: thesis: [x,y] in [:X,Y:]

then [x,y] in R by RELAT_1:def 11;

hence [x,y] in [:X,Y:] ; :: thesis: verum