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