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