let X be set ; :: thesis: for R being Relation holds dom (R | X) c= dom R
let R be Relation; :: thesis: dom (R | X) c= dom R
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (R | X) or x in dom R )
thus ( not x in dom (R | X) or x in dom R ) by Th86; :: thesis: verum