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
X | R c= R by Th117;
hence dom (X | R) c= dom R by Th25; :: thesis: verum