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