let X be set ; :: thesis: for R being Relation holds dom (X | R) c= dom R
let R be Relation; :: thesis: dom (X | R) c= dom R
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (X | R) or x in dom R )
assume x in dom (X | R) ; :: thesis: x in dom R
then consider y being set such that
A1: [x,y] in X | R by RELAT_1:def 4;
[x,y] in R by A1, RELAT_1:def 12;
hence x in dom R by RELAT_1:def 4; :: thesis: verum