set IR = the InternalRel of R;
set CR = the carrier of R;
R is reflexive by A1;
then A2: the InternalRel of R is_reflexive_in the carrier of R ;
R is transitive by A1;
then A3: the InternalRel of R is_transitive_in the carrier of R ;
then A4: the InternalRel of R quasi_orders the carrier of R by A2;
A5: the InternalRel of R /\ ( the InternalRel of R ~) is_reflexive_in the carrier of R

proof

let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in the carrier of R or [x,x] in the InternalRel of R /\ ( the InternalRel of R ~) )
assume x in the carrier of R ; :: thesis: [x,x] in the InternalRel of R /\ ( the InternalRel of R ~)
then A6: [x,x] in the InternalRel of R by A2;
then [x,x] in the InternalRel of R ~ by RELAT_1:def 7;
hence [x,x] in the InternalRel of R /\ ( the InternalRel of R ~) by A6, XBOOLE_0:def 4; :: thesis: verum

end;

then A7: dom ( the InternalRel of R /\ ( the InternalRel of R ~)) = the carrier of R by ORDERS_1:13;
A8: field ( the InternalRel of R /\ ( the InternalRel of R ~)) = the carrier of R by A5, ORDERS_1:13;
A9: the InternalRel of R /\ ( the InternalRel of R ~) is_symmetric_in the carrier of R

proof

let x, y be object ; :: according to RELAT_2:def 3 :: thesis: ( not x in the carrier of R or not y in the carrier of R or not [x,y] in the InternalRel of R /\ ( the InternalRel of R ~) or [y,x] in the InternalRel of R /\ ( the InternalRel of R ~) )
assume that
x in the carrier of R and
y in the carrier of R and
A10: [x,y] in the InternalRel of R /\ ( the InternalRel of R ~) ; :: thesis: [y,x] in the InternalRel of R /\ ( the InternalRel of R ~)
A11: [x,y] in the InternalRel of R by A10, XBOOLE_0:def 4;
A12: [x,y] in the InternalRel of R ~ by A10, XBOOLE_0:def 4;
A13: [y,x] in the InternalRel of R ~ by A11, RELAT_1:def 7;
[y,x] in the InternalRel of R by A12, RELAT_1:def 7;
hence [y,x] in the InternalRel of R /\ ( the InternalRel of R ~) by A13, XBOOLE_0:def 4; :: thesis: verum

end;

the InternalRel of R /\ ( the InternalRel of R ~) is_transitive_in the carrier of R

proof

let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in the carrier of R or not y in the carrier of R or not z in the carrier of R or not [x,y] in the InternalRel of R /\ ( the InternalRel of R ~) or not [y,z] in the InternalRel of R /\ ( the InternalRel of R ~) or [x,z] in the InternalRel of R /\ ( the InternalRel of R ~) )
assume that
A14: x in the carrier of R and
A15: y in the carrier of R and
A16: z in the carrier of R and
A17: [x,y] in the InternalRel of R /\ ( the InternalRel of R ~) and
A18: [y,z] in the InternalRel of R /\ ( the InternalRel of R ~) ; :: thesis: [x,z] in the InternalRel of R /\ ( the InternalRel of R ~)
A19: [x,y] in the InternalRel of R by A17, XBOOLE_0:def 4;
A20: [x,y] in the InternalRel of R ~ by A17, XBOOLE_0:def 4;
A21: [y,z] in the InternalRel of R by A18, XBOOLE_0:def 4;
A22: [y,z] in the InternalRel of R ~ by A18, XBOOLE_0:def 4;
A23: [x,z] in the InternalRel of R by A3, A14, A15, A16, A19, A21;
the InternalRel of R ~ quasi_orders the carrier of R by A4, ORDERS_1:40;
then the InternalRel of R ~ is_transitive_in the carrier of R ;
then [x,z] in the InternalRel of R ~ by A14, A15, A16, A20, A22;
hence [x,z] in the InternalRel of R /\ ( the InternalRel of R ~) by A23, XBOOLE_0:def 4; :: thesis: verum

end;

hence the InternalRel of R /\ ( the InternalRel of R ~) is Equivalence_Relation of the carrier of R by A7, A8, A9, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum