let R be non empty reflexive transitive RelStr ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: [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 S_{1}[ 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 S_{1}[k] holds

S_{1}[k + 1]

then A10: S_{1}[1]
by A1;

A11: for k being non zero Nat holds S_{1}[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; :: thesis: verum

[x,y] in the InternalRel of R

let x, y be Element of R; :: thesis: ( 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 ; :: thesis: [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 S

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 S

S

proof

the InternalRel of R is_reflexive_in the carrier of R
by ORDERS_2:def 2;
let k be non zero Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: S_{1}[k]
; :: thesis: S_{1}[k + 1]

assume A6: k + 1 in dom p ; :: thesis: [(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; :: thesis: verum

end;assume A5: S

assume A6: k + 1 in dom p ; :: thesis: [(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; :: thesis: verum

then A10: S

A11: for k being non zero Nat holds S

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; :: thesis: verum