let R be Relation; :: thesis: for X being set holds
( (R | X) ~ = X |` (R ~) & (X |` R) ~ = (R ~) | X )
let X be set ; :: thesis: ( (R | X) ~ = X |` (R ~) & (X |` R) ~ = (R ~) | X )
thus (R | X) ~ = X |` (R ~) by Lm1; :: thesis: (X |` R) ~ = (R ~) | X
((R ~) | X) ~ = X |` ((R ~) ~) by Lm1;
hence (X |` R) ~ = (R ~) | X ; :: thesis: verum