let X be non empty set ; for R being total reflexive Relation of X holds Aux R = (((R ~) `) /\ (R `)) \/ (((R `) ~) /\ ((R `) \/ (R ~)))
let R be total reflexive Relation of X; Aux R = (((R ~) `) /\ (R `)) \/ (((R `) ~) /\ ((R `) \/ (R ~)))
set Z1 = (((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) ` ;
z1: (((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) ` =
(((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) `) /\ ((R /\ (R ~)) `)
by XBOOLE_1:53
.=
(((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) `) /\ ((R `) \/ ((R ~) `))
by XBOOLE_1:54
.=
(((R /\ ((R ~) `)) `) /\ (((R /\ ((R ~) `)) ~) `)) /\ ((R `) \/ ((R ~) `))
by XBOOLE_1:53
.=
(((R `) \/ (((R ~) `) `)) /\ (((R /\ ((R ~) `)) ~) `)) /\ ((R `) \/ ((R ~) `))
by XBOOLE_1:54
.=
(((R `) \/ (((R ~) `) `)) /\ (((R ~) /\ (((R ~) `) ~)) `)) /\ ((R `) \/ ((R ~) `))
by RELAT_1:22
.=
((((R ~) `) \/ ((((R ~) `) ~) `)) /\ ((R `) \/ (R ~))) /\ ((R `) \/ ((R ~) `))
by XBOOLE_1:54
.=
(((R ~) `) \/ ((((R ~) `) ~) `)) /\ (((R `) \/ (R ~)) /\ ((R `) \/ ((R ~) `)))
by XBOOLE_1:16
.=
(((R ~) `) \/ ((((R ~) `) ~) `)) /\ ((R `) \/ ((R ~) /\ ((R ~) `)))
by XBOOLE_1:24
.=
(((R ~) `) \/ ((((R ~) `) ~) `)) /\ ((R `) \/ {})
by XBOOLE_0:def 7, SUBSET_1:23
.=
(((R ~) `) \/ R) /\ (R `)
by Tilde1
;
set Z2 = ((((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) `) ~ ;
z2: ((((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) `) ~ =
((((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) `) /\ ((R /\ (R ~)) `)) ~
by XBOOLE_1:53
.=
((((R /\ ((R ~) `)) `) /\ (((R /\ ((R ~) `)) ~) `)) /\ ((R /\ (R ~)) `)) ~
by XBOOLE_1:53
.=
((((R `) \/ (((R ~) `) `)) /\ (((R /\ ((R ~) `)) ~) `)) /\ ((R /\ (R ~)) `)) ~
by XBOOLE_1:54
.=
((((R `) \/ (R ~)) /\ (((R /\ ((R ~) `)) ~) `)) ~) /\ (((R /\ (R ~)) `) ~)
by RELAT_1:22
.=
((((R `) \/ (R ~)) ~) /\ ((((R /\ ((R ~) `)) ~) `) ~)) /\ (((R /\ (R ~)) `) ~)
by RELAT_1:22
.=
((((R `) ~) \/ ((R ~) ~)) /\ ((((R /\ ((R ~) `)) ~) `) ~)) /\ (((R /\ (R ~)) `) ~)
by RELAT_1:23
.=
((((R `) ~) \/ R) /\ ((((R /\ ((R ~) `)) ~) `) ~)) /\ (((R `) \/ ((R ~) `)) ~)
by XBOOLE_1:54
.=
((((R `) ~) \/ R) /\ ((((R /\ ((R ~) `)) ~) `) ~)) /\ (((R `) ~) \/ (((R ~) `) ~))
by RELAT_1:23
.=
((((R `) ~) \/ R) /\ ((((R ~) /\ (((R ~) `) ~)) `) ~)) /\ (((R `) ~) \/ (((R ~) `) ~))
by RELAT_1:22
.=
((((R `) ~) \/ R) /\ ((((R ~) `) \/ ((((R ~) `) ~) `)) ~)) /\ (((R `) ~) \/ (((R ~) `) ~))
by XBOOLE_1:54
.=
((((R `) ~) \/ R) /\ ((((R ~) `) ~) \/ (((((R ~) `) ~) `) ~))) /\ (((R `) ~) \/ (((R ~) `) ~))
by RELAT_1:23
.=
((((R `) ~) \/ R) /\ ((((R ~) `) ~) \/ (R ~))) /\ (((R `) ~) \/ (((R ~) `) ~))
by Tilde1
.=
((((R `) ~) \/ R) /\ ((R `) \/ (R ~))) /\ (((R `) ~) \/ (((R ~) `) ~))
by Tilde3
.=
((((R `) ~) \/ R) /\ ((R `) \/ (R ~))) /\ (((R `) ~) \/ (R `))
by Tilde3
.=
((((R `) ~) \/ (R `)) /\ (((R `) ~) \/ R)) /\ ((R `) \/ (R ~))
by XBOOLE_1:16
.=
(((R `) ~) \/ ((R `) /\ R)) /\ ((R `) \/ (R ~))
by XBOOLE_1:24
.=
(((R `) ~) \/ {}) /\ ((R `) \/ (R ~))
by XBOOLE_0:def 7, SUBSET_1:23
.=
((R `) ~) /\ ((R `) \/ (R ~))
;
Aux R =
((((R ~) `) /\ (R `)) \/ (R /\ (R `))) \/ (((R `) ~) /\ ((R `) \/ (R ~)))
by z1, z2, XBOOLE_1:23
.=
((((R ~) `) /\ (R `)) \/ {}) \/ (((R `) ~) /\ ((R `) \/ (R ~)))
by XBOOLE_0:def 7, SUBSET_1:23
.=
(((R ~) `) /\ (R `)) \/ (((R `) ~) /\ ((R `) \/ (R ~)))
;
hence
Aux R = (((R ~) `) /\ (R `)) \/ (((R `) ~) /\ ((R `) \/ (R ~)))
; verum