let X be non empty set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( [x,y] in id (field (Aux R)) implies [x,y] in R /\ (R ~) )
assume [x,y] in id (field (Aux R)) ; :: thesis: [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; :: thesis: 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; :: thesis: verum