let G be _Graph; :: thesis: for W being Walk of G

for n being odd Element of NAT st n < len W holds

( n in dom W & n + 1 in dom W & n + 2 in dom W )

let W be Walk of G; :: thesis: for n being odd Element of NAT st n < len W holds

( n in dom W & n + 1 in dom W & n + 2 in dom W )

let n be odd Element of NAT ; :: thesis: ( n < len W implies ( n in dom W & n + 1 in dom W & n + 2 in dom W ) )

A1: 1 <= n by ABIAN:12;

A2: 1 <= n + 1 by NAT_1:12;

A3: 1 <= n + 2 by NAT_1:12;

assume A4: n < len W ; :: thesis: ( n in dom W & n + 1 in dom W & n + 2 in dom W )

then A5: n + 1 <= len W by NAT_1:13;

n + 2 <= len W by A4, Th1;

hence ( n in dom W & n + 1 in dom W & n + 2 in dom W ) by A4, A1, A2, A3, A5, FINSEQ_3:25; :: thesis: verum

for n being odd Element of NAT st n < len W holds

( n in dom W & n + 1 in dom W & n + 2 in dom W )

let W be Walk of G; :: thesis: for n being odd Element of NAT st n < len W holds

( n in dom W & n + 1 in dom W & n + 2 in dom W )

let n be odd Element of NAT ; :: thesis: ( n < len W implies ( n in dom W & n + 1 in dom W & n + 2 in dom W ) )

A1: 1 <= n by ABIAN:12;

A2: 1 <= n + 1 by NAT_1:12;

A3: 1 <= n + 2 by NAT_1:12;

assume A4: n < len W ; :: thesis: ( n in dom W & n + 1 in dom W & n + 2 in dom W )

then A5: n + 1 <= len W by NAT_1:13;

n + 2 <= len W by A4, Th1;

hence ( n in dom W & n + 1 in dom W & n + 2 in dom W ) by A4, A1, A2, A3, A5, FINSEQ_3:25; :: thesis: verum