let X be non empty set ; :: thesis: for R being Relation of X holds (((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) \/ (Aux R) = nabla X
let R be Relation of X; :: thesis: (((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) \/ (Aux R) = nabla X
set P = R /\ ((R ~) `);
set J = R /\ (R ~);
(((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) ` c= Aux R by XBOOLE_1:7;
then (((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) \/ ((((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) `) c= (((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) \/ (Aux R) by XBOOLE_1:13;
then [#] [:X,X:] c= (((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) \/ (Aux R) by SUBSET_1:10;
hence (((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) \/ (Aux R) = nabla X by XBOOLE_0:def 10; :: thesis: verum