let Y be set ; :: thesis: for R being Relation holds Y | R c= R
let R be Relation; :: thesis: Y | R c= R
thus for x, y being set st [x,y] in Y | R holds
[x,y] in R by Def12; :: according to RELAT_1:def 3 :: thesis: verum