let Y be set ; for R being Relation holds Y |` R c= R | (R " Y)
let R be Relation; Y |` R c= R | (R " Y)
let a, b be object ; RELAT_1:def 3 ( [a,b] in Y |` R implies [a,b] in R | (R " Y) )
assume A1:
[a,b] in Y |` R
; [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; verum