let P, R be Relation; :: thesis: dom (P * R) c= dom P
let x be set ; :: 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 set such that
A1: [x,y] in P * R by Def4;
ex z being set st
( [x,z] in P & [z,y] in R ) by A1, Def8;
hence x in dom P by Def4; :: thesis: verum