let X be set ; :: thesis: for R being Relation holds (R | X) | X = R | X
let R be Relation; :: thesis: (R | X) | X = R | X
X /\ X = X ;
hence (R | X) | X = R | X by Th100; :: thesis: verum