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;
( the InternalRel of R /\ (the InternalRel of R ~ ) is total & the InternalRel of R /\ (the InternalRel of R ~ ) is symmetric & the InternalRel of R /\ (the InternalRel of R ~ ) is transitive )
proof
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 &
field (the InternalRel of R /\ (the InternalRel of R ~ )) = the
carrier of
R )
by ORDERS_1:98;
hence
the
InternalRel of
R /\ (the InternalRel of R ~ ) is
total
by PARTFUN1:def 4;
:: thesis: ( the InternalRel of R /\ (the InternalRel of R ~ ) is symmetric & the InternalRel of R /\ (the InternalRel of R ~ ) is transitive )
the
InternalRel of
R /\ (the InternalRel of R ~ ) is_symmetric_in the
carrier of
R
proof
let x,
y be
set ;
:: 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 &
y in the
carrier of
R )
and A8:
[x,y] in the
InternalRel of
R /\ (the InternalRel of R ~ )
;
:: thesis: [y,x] in the InternalRel of R /\ (the InternalRel of R ~ )
(
[x,y] in the
InternalRel of
R &
[x,y] in the
InternalRel of
R ~ )
by A8, XBOOLE_0:def 4;
then
(
[y,x] in the
InternalRel of
R ~ &
[y,x] in the
InternalRel of
R )
by RELAT_1:def 7;
hence
[y,x] in the
InternalRel of
R /\ (the InternalRel of R ~ )
by XBOOLE_0:def 4;
:: thesis: verum
end;
hence
the
InternalRel of
R /\ (the InternalRel of R ~ ) is
symmetric
by A7, RELAT_2:def 11;
:: thesis: the InternalRel of R /\ (the InternalRel of R ~ ) is transitive
the
InternalRel of
R /\ (the InternalRel of R ~ ) is_transitive_in the
carrier of
R
proof
let x,
y,
z be
set ;
:: 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 A9:
x in the
carrier of
R
and A10:
y in the
carrier of
R
and A11:
z in the
carrier of
R
and A12:
[x,y] in the
InternalRel of
R /\ (the InternalRel of R ~ )
and A13:
[y,z] in the
InternalRel of
R /\ (the InternalRel of R ~ )
;
:: thesis: [x,z] in the InternalRel of R /\ (the InternalRel of R ~ )
A14:
(
[x,y] in the
InternalRel of
R &
[x,y] in the
InternalRel of
R ~ )
by A12, XBOOLE_0:def 4;
A15:
(
[y,z] in the
InternalRel of
R &
[y,z] in the
InternalRel of
R ~ )
by A13, XBOOLE_0:def 4;
then A16:
[x,z] in the
InternalRel of
R
by A3, A9, A10, A11, A14, 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 A9, A10, A11, A14, A15, RELAT_2:def 8;
hence
[x,z] in the
InternalRel of
R /\ (the InternalRel of R ~ )
by A16, XBOOLE_0:def 4;
:: thesis: verum
end;
hence
the
InternalRel of
R /\ (the InternalRel of R ~ ) is
transitive
by A7, RELAT_2:def 16;
:: thesis: verum
end;
hence
the InternalRel of R /\ (the InternalRel of R ~ ) is Equivalence_Relation of the carrier of R
; :: thesis: verum