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 set ; :: according to RELAT_1:def 3 :: thesis: ( not [a,b] in Y | R or [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 RELAT_1:def 12;
A3: [a,b] in R by A1, RELAT_1:def 12;
then a in R " Y by A2, RELAT_1:def 14;
hence [a,b] in R | (R " Y) by A3, RELAT_1:def 11; :: thesis: verum