for X being non empty set
for R being Relation of X holds (((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) \/ (Aux R) = nabla X