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