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 ~)))) by XBOOLE_0:def 7, SUBSET_1:23
.= R /\ ((R ~) /\ (((R `) ~) /\ ((R `) \/ (R ~)))) by XBOOLE_1:16
.= R /\ (((R ~) /\ ((R `) ~)) /\ ((R `) \/ (R ~))) by XBOOLE_1:16
.= (R /\ ((R ~) /\ ((R `) ~))) /\ ((R `) \/ (R ~)) by XBOOLE_1:16
.= ((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 ~)) 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 `) /\ R) ~) by RELAT_1:22
.= R /\ ({} ~) by XBOOLE_0:def 7, SUBSET_1:23
.= {} ;
hence R /\ (R ~) misses Aux R by XBOOLE_0:def 7; :: thesis: verum