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

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