let Y be set ; :: thesis: for R being Relation holds Y |` R c= R | (R " Y)
let R be Relation; :: thesis: Y |` R c= R | (R " Y)
let a, b be object ; :: according to RELAT_1:def 3 :: thesis: ( [a,b] in Y |` R implies [a,b] in R | (R " Y) )
assume A1: [a,b] in Y |` R ; :: thesis: [a,b] in R | (R " Y)
then A2: b in Y by Def10;
A3: [a,b] in R by A1, Def10;
then a in R " Y by A2, Def12;
hence [a,b] in R | (R " Y) by A3, Def9; :: thesis: verum