let X be set ; :: thesis: for R being Relation holds R |_2 X = X | (R | X)
let R be Relation; :: thesis: R |_2 X = X | (R | X)
thus R |_2 X = (X | R) | X by Th17
.= X | (R | X) by RELAT_1:109 ; :: thesis: verum