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