set IR = the InternalRel of R;
set CR = the carrier of R;
R is reflexive
by A1, Def3;
then A2:
the InternalRel of R is_reflexive_in the carrier of R
by ORDERS_2:def 4;
R is transitive
by A1, Def3;
then A3:
the InternalRel of R is_transitive_in the carrier of R
by ORDERS_2:def 5;
then A4:
the InternalRel of R quasi_orders the carrier of R
by A2, ORDERS_1:def 6;
A5:
the InternalRel of R /\ (the InternalRel of R ~ ) is_reflexive_in the carrier of R
then A7:
dom (the InternalRel of R /\ (the InternalRel of R ~ )) = the carrier of R
by ORDERS_1:98;
A8:
field (the InternalRel of R /\ (the InternalRel of R ~ )) = the carrier of R
by A5, ORDERS_1:98;
A9:
the InternalRel of R /\ (the InternalRel of R ~ ) is_symmetric_in the carrier of R
proof
let x,
y be
set ;
RELAT_2:def 3 ( 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 ~ )
;
[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;
verum
end;
the InternalRel of R /\ (the InternalRel of R ~ ) is_transitive_in the carrier of R
proof
let x,
y,
z be
set ;
RELAT_2:def 8 ( 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 ~ )
;
[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, RELAT_2:def 8;
the
InternalRel of
R ~ quasi_orders the
carrier of
R
by A4, ORDERS_1:136;
then
the
InternalRel of
R ~ is_transitive_in the
carrier of
R
by ORDERS_1:def 6;
then
[x,z] in the
InternalRel of
R ~
by A14, A15, A16, A20, A22, RELAT_2:def 8;
hence
[x,z] in the
InternalRel of
R /\ (the InternalRel of R ~ )
by A23, XBOOLE_0:def 4;
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 4, RELAT_2:def 11, RELAT_2:def 16; verum