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