let X be non empty set ; :: thesis: for R being total reflexive Relation of X holds R /\ ((R ~) `),R /\ (R ~), Aux R are_mutually_disjoint
let R be total reflexive Relation of X; :: thesis: R /\ ((R ~) `),R /\ (R ~), Aux R are_mutually_disjoint
set A = R /\ ((R ~) `);
set B = R /\ (R ~);
set C = Aux R;
(R /\ ((R ~) `)) /\ (R /\ (R ~)) = R /\ (((R ~) `) /\ (R ~)) by XBOOLE_1:116
.= R /\ {} by XBOOLE_0:def 7, SUBSET_1:23
.= {} ;
hence R /\ ((R ~) `),R /\ (R ~), Aux R are_mutually_disjoint by AuxEq3, XBOOLE_0:def 7, AuxEq2; :: thesis: verum