let G be _Graph; :: thesis: for W being Walk of G
for u, e, v being object st e Joins u,v,G & G .walkOf (u,e,v) is_odd_substring_of W, 0 holds
( e in W .edges() & u in W .vertices() & v in W .vertices() )
let W be Walk of G; :: thesis: for u, e, v being object st e Joins u,v,G & G .walkOf (u,e,v) is_odd_substring_of W, 0 holds
( e in W .edges() & u in W .vertices() & v in W .vertices() )
let u, e, v be object ; :: thesis: ( e Joins u,v,G & G .walkOf (u,e,v) is_odd_substring_of W, 0 implies ( e in W .edges() & u in W .vertices() & v in W .vertices() ) )
set W2 = G .walkOf (u,e,v);
assume ( e Joins u,v,G & G .walkOf (u,e,v) is_odd_substring_of W, 0 ) ; :: thesis: ( e in W .edges() & u in W .vertices() & v in W .vertices() )
then A1: ( e Joins u,v,G & G .walkOf (u,e,v) is_odd_substring_of W,1 ) by Th18;
then A2: len (G .walkOf (u,e,v)) = 3 by GLIB_001:14;
consider i being odd Nat such that
A4: ( 1 <= i & i <= len W & mid (W,i,((i -' 1) + (len (G .walkOf (u,e,v))))) = G .walkOf (u,e,v) ) by A1;
set j = (i -' 1) + (len (G .walkOf (u,e,v)));
set M = (the_Vertices_of G) \/ (the_Edges_of G);
G .walkOf (u,e,v) is_odd_substring_of W,i by A4;
then G .walkOf (u,e,v) is_substring_of W,i by Th12;
then A5: ( 1 <= (i -' 1) + (len (G .walkOf (u,e,v))) & (i -' 1) + (len (G .walkOf (u,e,v))) <= len W & i <= (i -' 1) + (len (G .walkOf (u,e,v))) ) by Th11;
len (mid (W,i,((i -' 1) + (len (G .walkOf (u,e,v)))))) = 3 by A1, A4, GLIB_001:14;
then A8: ( (mid (W,i,((i -' 1) + (len (G .walkOf (u,e,v)))))) . 1 = W . ((1 + i) -' 1) & (mid (W,i,((i -' 1) + (len (G .walkOf (u,e,v)))))) . 2 = W . ((2 + i) -' 1) & (mid (W,i,((i -' 1) + (len (G .walkOf (u,e,v)))))) . 3 = W . ((3 + i) -' 1) ) by A4, A5, FINSEQ_6:118;
( (1 + i) -' 1 = (1 + i) - 1 & (2 + i) -' 1 = (2 + i) - 1 & (3 + i) -' 1 = (3 + i) - 1 ) by NAT_D:37;
then A9: ( (G .walkOf (u,e,v)) . 1 = W . i & (G .walkOf (u,e,v)) . 2 = W . (i + 1) & (G .walkOf (u,e,v)) . 3 = W . (i + 2) ) by A8, A4;
G .walkOf (u,e,v) = <*u,e,v*> by A1, GLIB_001:def 5;
then A10: ( W . i = u & W . (i + 1) = e & W . (i + 2) = v ) by A9, FINSEQ_1:45;
(i -' 1) + (len (G .walkOf (u,e,v))) = (i + 3) -' 1 by A2, A4, NAT_D:38
.= (i + 3) - 1 by NAT_D:37
.= i + 2 ;
then A11: ( 1 <= i + 2 & i + 2 <= len W ) by A5;
( i + 0 <= i + 1 & i + 1 <= i + 2 ) by XREAL_1:6;
then A12: ( 1 <= i + 1 & i + 1 <= len W ) by A4, A11, XXREAL_0:2;
reconsider k = i + 1 as even Element of NAT ;
reconsider l = i + 2 as odd Element of NAT ;
thus e in W .edges() by A12, A10, GLIB_001:99; :: thesis: ( u in W .vertices() & v in W .vertices() )
i in NAT by ORDINAL1:def 12;
hence u in W .vertices() by A4, A10, GLIB_001:87; :: thesis: v in W .vertices()
thus v in W .vertices() by A11, A10, GLIB_001:87; :: thesis: verum