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 Th10
.= X |` (R | X) by RELAT_1:109 ; :: thesis: verum