set IR = the InternalRel of R;
set CR = the carrier of R;
R is reflexive
by B1, Def3;
then A1:
the InternalRel of R is_reflexive_in the carrier of R
by ORDERS_2:def 2;
R is transitive
by B1, Def3;
then A2:
the InternalRel of R is_transitive_in the carrier of R
by ORDERS_2:def 3;
then A3:
the InternalRel of R quasi_orders the carrier of R
by A1, ORDERS_1:def 6;
A4:
the InternalRel of R /\ ( the InternalRel of R ~) is_reflexive_in the carrier of R
then A6:
dom ( the InternalRel of R /\ ( the InternalRel of R ~)) = the carrier of R
by ORDERS_1:13;
A7:
field ( the InternalRel of R /\ ( the InternalRel of R ~)) = the carrier of R
by A4, ORDERS_1:13;
A8:
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 A9:
[x,y] in the
InternalRel of
R /\ ( the InternalRel of R ~)
;
[y,x] in the InternalRel of R /\ ( the InternalRel of R ~)
A10:
[x,y] in the
InternalRel of
R
by A9, XBOOLE_0:def 4;
A11:
[x,y] in the
InternalRel of
R ~
by A9, XBOOLE_0:def 4;
A12:
[y,x] in the
InternalRel of
R ~
by A10, RELAT_1:def 7;
[y,x] in the
InternalRel of
R
by A11, RELAT_1:def 7;
hence
[y,x] in the
InternalRel of
R /\ ( the InternalRel of R ~)
by A12, 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 A13:
x in the
carrier of
R
and A14:
y in the
carrier of
R
and A15:
z in the
carrier of
R
and A16:
[x,y] in the
InternalRel of
R /\ ( the InternalRel of R ~)
and A17:
[y,z] in the
InternalRel of
R /\ ( the InternalRel of R ~)
;
[x,z] in the InternalRel of R /\ ( the InternalRel of R ~)
A18:
[x,y] in the
InternalRel of
R
by A16, XBOOLE_0:def 4;
A19:
[x,y] in the
InternalRel of
R ~
by A16, XBOOLE_0:def 4;
A20:
[y,z] in the
InternalRel of
R
by A17, XBOOLE_0:def 4;
A21:
[y,z] in the
InternalRel of
R ~
by A17, XBOOLE_0:def 4;
A22:
[x,z] in the
InternalRel of
R
by A2, A13, A14, A15, A18, A20, RELAT_2:def 8;
the
InternalRel of
R ~ quasi_orders the
carrier of
R
by A3, ORDERS_1:40;
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 A13, A14, A15, A19, A21, RELAT_2:def 8;
hence
[x,z] in the
InternalRel of
R /\ ( the InternalRel of R ~)
by A22, XBOOLE_0:def 4;
verum
end;
hence
the InternalRel of R /\ ( the InternalRel of R ~) is Equivalence_Relation of the carrier of R
by A6, A7, A8, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16; verum