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 object ; :: 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 object such that
A1: [x,y] in X |` R by XTUPLE_0:def 12;
[x,y] in R by A1, RELAT_1:def 12;
hence x in dom R by XTUPLE_0:def 12; :: thesis: verum