let R be non empty reflexive transitive RelStr ; for x, y being Element of R st the InternalRel of R reduces x,y holds
[x,y] in the InternalRel of R
let x, y be Element of R; ( the InternalRel of R reduces x,y implies [x,y] in the InternalRel of R )
set cR = the carrier of R;
set IR = the InternalRel of R;
assume
the InternalRel of R reduces x,y
; [x,y] in the InternalRel of R
then consider p being RedSequence of the InternalRel of R such that
A1:
p . 1 = x
and
A2:
p . (len p) = y
by REWRITE1:def 3;
reconsider p = p as FinSequence ;
defpred S1[ Nat] means ( $1 in dom p implies [(p . 1),(p . $1)] in the InternalRel of R );
A3:
the InternalRel of R is_transitive_in the carrier of R
by ORDERS_2:def 3;
A4:
for k being non zero Nat st S1[k] holds
S1[k + 1]
proof
let k be non
zero Nat;
( S1[k] implies S1[k + 1] )
assume A5:
S1[
k]
;
S1[k + 1]
assume A6:
k + 1
in dom p
;
[(p . 1),(p . (k + 1))] in the InternalRel of R
then
(
k <= k + 1 &
k + 1
<= len p )
by FINSEQ_3:25, NAT_1:11;
then A7:
(
0 + 1
<= k &
k <= len p )
by NAT_1:13;
then A8:
p . 1
in the
carrier of
R
by A5, FINSEQ_3:25, ZFMISC_1:87;
k in dom p
by A7, FINSEQ_3:25;
then A9:
[(p . k),(p . (k + 1))] in the
InternalRel of
R
by A6, REWRITE1:def 2;
then
(
p . k in the
carrier of
R &
p . (k + 1) in the
carrier of
R )
by ZFMISC_1:87;
hence
[(p . 1),(p . (k + 1))] in the
InternalRel of
R
by A3, A5, A7, A9, A8, FINSEQ_3:25;
verum
end;
the InternalRel of R is_reflexive_in the carrier of R
by ORDERS_2:def 2;
then A10:
S1[1]
by A1;
A11:
for k being non zero Nat holds S1[k]
from NAT_1:sch 10(A10, A4);
A12:
len p > 0
by REWRITE1:def 2;
then
0 + 1 <= len p
by NAT_1:13;
then
len p in dom p
by FINSEQ_3:25;
hence
[x,y] in the InternalRel of R
by A1, A2, A12, A11; verum