let G be _Graph; :: thesis: for W being Walk of G
for n being odd Element of NAT st n + 2 <= len W holds
G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) is_odd_substring_of W, 0
let W be Walk of G; :: thesis: for n being odd Element of NAT st n + 2 <= len W holds
G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) is_odd_substring_of W, 0
let n be odd Element of NAT ; :: thesis: ( n + 2 <= len W implies G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) is_odd_substring_of W, 0 )
assume A1: n + 2 <= len W ; :: thesis: G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) is_odd_substring_of W, 0
then A2: n < len W by GLIB_001:1;
set W2 = G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2)));

now :: thesis: ( len (G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2)))) > 0 implies ex n being odd Element of NAT st
( 0 <= n & n <= len W & mid (W,n,((n -' 1) + (len (G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))))))) = G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) ) )

assume len (G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2)))) > 0 ; :: thesis: ex n being odd Element of NAT st
( 0 <= n & n <= len W & mid (W,n,((n -' 1) + (len (G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))))))) = G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) )
take n = n; :: thesis: ( 0 <= n & n <= len W & mid (W,n,((n -' 1) + (len (G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))))))) = G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) )
thus 0 <= n ; :: thesis: ( n <= len W & mid (W,n,((n -' 1) + (len (G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))))))) = G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) )
(n + 2) - 2 <= (len W) - 0 by A1, XREAL_1:13;
hence A3: n <= len W ; :: thesis: mid (W,n,((n -' 1) + (len (G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))))))) = G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2)))
A5: W . (n + 1) Joins W . n,W . (n + 2),G by A2, GLIB_001:def 3;
then A6: (n -' 1) + (len (G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))))) = (n -' 1) + 3 by GLIB_001:14
.= (n + 3) -' 1 by ABIAN:12, NAT_D:38
.= (n + 3) - 1 by NAT_D:37
.= n + 2 ;
1 <= n by ABIAN:12;
then n in dom W by A3, FINSEQ_3:25;
then mid (W,n,(n + 2)) = <*(W . n),(W . (n + 1)),(W . (n + 2))*> by A1, Th10;
hence mid (W,n,((n -' 1) + (len (G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))))))) = G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) by A5, A6, GLIB_001:def 5; :: thesis: verum

end;

hence G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) is_odd_substring_of W, 0 ; :: thesis: verum