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
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 ;
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
object ;
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;
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;
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; verum