let X be non empty set ; for R being total reflexive Relation of X holds
( Aux R is irreflexive & Aux R is symmetric )
let R be total reflexive Relation of X; ( Aux R is irreflexive & Aux R is symmetric )
set P = R /\ ((R ~) `);
set T = R /\ (R ~);
set C = (((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) ` ;
set Y = field (Aux R);
for x, y being object st [x,y] in id (field (Aux R)) holds
[x,y] in R /\ (R ~)
proof
let x,
y be
object ;
( [x,y] in id (field (Aux R)) implies [x,y] in R /\ (R ~) )
assume
[x,y] in id (field (Aux R))
;
[x,y] in R /\ (R ~)
then A0:
(
x in field (Aux R) &
x = y )
by RELAT_1:def 10;
field R = X
by ORDERS_1:12;
then A1:
[x,x] in R
by A0, RELAT_2:def 1, RELAT_2:def 9;
then
[x,x] in R ~
by RELAT_1:def 7;
hence
[x,y] in R /\ (R ~)
by A0, A1, XBOOLE_0:def 4;
verum
end;
then x4:
id (field (Aux R)) c= ((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))
by XBOOLE_1:10, RELAT_1:def 3;
then Y2:
(id (field (Aux R))) /\ ((((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) `) = {}
by XBOOLE_0:def 7, XBOOLE_1:85;
(id (field (Aux R))) ~ misses ((((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) `) ~
by x4, LemmaAuxIrr, XBOOLE_1:85;
then Y3:
(id (field (Aux R))) /\ (((((R /\ ((R ~) `)) \/ ((R /\ ((R ~) `)) ~)) \/ (R /\ (R ~))) `) ~) = {}
by XBOOLE_0:def 7;
(id (field (Aux R))) /\ (Aux R) = {} \/ {}
by Y2, Y3, XBOOLE_1:23;
hence
( Aux R is irreflexive & Aux R is symmetric )
by RELAT_2:2, XBOOLE_0:def 7; verum