for X being non empty set
for R being total reflexive Relation of X holds R /\ ((R ~) `),R /\ (R ~), Aux R are_mutually_disjoint