let X be non empty set ; :: thesis: for R being Relation of X holds R /\ ((R ~) `),R /\ (R ~),(R `) /\ ((R ~) `) are_mutually_disjoint
let R be Relation of X; :: thesis: R /\ ((R ~) `),R /\ (R ~),(R `) /\ ((R ~) `) are_mutually_disjoint
set C = (R `) /\ ((R ~) `);
z1: (R /\ ((R ~) `)) /\ (R /\ (R ~)) = R /\ (((R ~) `) /\ (R ~)) by XBOOLE_1:116
.= R /\ {} by XBOOLE_0:def 7, SUBSET_1:23
.= {} ;
z2: (R /\ ((R ~) `)) /\ ((R `) /\ ((R ~) `)) = ((R ~) `) /\ (R /\ (R `)) by XBOOLE_1:116
.= ((R ~) `) /\ {} by XBOOLE_0:def 7, SUBSET_1:23
.= {} ;
X0: R /\ (R `) = {} by XBOOLE_0:def 7, SUBSET_1:23;
(R /\ (R ~)) /\ ((R `) /\ ((R ~) `)) = (R /\ ((R `) /\ ((R ~) `))) /\ (R ~) by XBOOLE_1:16
.= ((R /\ (R `)) /\ ((R ~) `)) /\ (R ~) by XBOOLE_1:16
.= {} by X0 ;
hence R /\ ((R ~) `),R /\ (R ~),(R `) /\ ((R ~) `) are_mutually_disjoint by z1, z2, XBOOLE_0:def 7; :: thesis: verum