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

( (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