let X be set ; :: thesis: for R being X -defined Relation holds R = R | X
let R be X -defined Relation; :: thesis: R = R | X
dom R c= X by Def18;
hence R | X = R by Th97; :: thesis: verum