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 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; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[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 ;
then A7: ( 0 + 1 <= k & k <= len p ) by NAT_1:13;
then A8: p . 1 in the carrier of R by ;
k in dom p by ;
then A9: [(p . k),(p . (k + 1))] in the InternalRel of R by ;
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 ; :: thesis: 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 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