let n, i, j be Element of NAT ; :: thesis:
assume ( i <= n & j <= n ) ; :: thesis:
then consider fs1 being FinSequence of NAT such that
A1: ( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) by Th6;
for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 holds
fs1 /. i1,fs1 /. (i1 + 1) are_adjacent1

let i1 be Element of NAT ; :: thesis:
assume A2: ( 1 <= i1 & i1 < len fs1 ) ; :: thesis:
then ( 1 <= i1 + 1 & i1 + 1 <= len fs1 ) by NAT_1:13;
then A3: fs1 . (i1 + 1) = fs1 /. (i1 + 1) by FINSEQ_4:24;
A4: fs1 . i1 = fs1 /. i1 by A2, FINSEQ_4:24;
( fs1 . (i1 + 1) = (fs1 /. i1) + 1 or fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) by A1, A2;
hence fs1 /. i1,fs1 /. (i1 + 1) are_adjacent1 by A3, A4, Def1; :: thesis:

end;

hence ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 holds
fs1 /. i1,fs1 /. (i1 + 1) are_adjacent1 ) ) by A1; :: thesis: