let X, Y be set ; :: thesis: for R being Relation holds (R |_2 X) |_2 Y = (R |_2 Y) |_2 X
let R be Relation; :: thesis: (R |_2 X) |_2 Y = (R |_2 Y) |_2 X
thus (R |_2 X) |_2 Y = R |_2 (Y /\ X) by Th19
.= (R |_2 Y) |_2 X by Th19 ; :: thesis: verum