let P, R be Relation; :: thesis: dom (P * R) c= dom P
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (P * R) or x in dom P )
assume x in dom (P * R) ; :: thesis: x in dom P
then consider y being object such that
A1: [x,y] in P * R by XTUPLE_0:def 12;
ex z being object st
( [x,z] in P & [z,y] in R ) by A1, Def6;
hence x in dom P by XTUPLE_0:def 12; :: thesis: verum