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 ) )
assume A1: n < len W ; :: thesis: ( n in dom W & n + 1 in dom W & n + 2 in dom W )
A2: 1 <= n by HEYTING3:1;
A3: ( 1 <= n + 1 & 1 <= n + 2 ) by NAT_1:12;
( n + 1 <= len W & n + 2 <= len W ) by A1, Th1, NAT_1:13;
hence ( n in dom W & n + 1 in dom W & n + 2 in dom W ) by A1, A2, A3, FINSEQ_3:27; :: thesis: verum