let X be non empty set ; for R being Relation of X holds R /\ ((R ~) `),R /\ (R ~),(R `) /\ ((R ~) `) are_mutually_disjoint
let R be Relation of X; 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; verum