let X be set ; for P, R being Relation st P c= R holds
P | X c= R | X
let P, R be Relation; ( P c= R implies P | X c= R | X )
assume A1:
P c= R
; P | X c= R | X
let x be object ; RELAT_1:def 3 for b being object st [x,b] in P | X holds
[x,b] in R | X
let y be object ; ( [x,y] in P | X implies [x,y] in R | X )
assume
[x,y] in P | X
; [x,y] in R | X
then
( [x,y] in P & x in X )
by Def9;
hence
[x,y] in R | X
by A1, Def9; verum