let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V
for W being Walk of G1 holds
( W .vertices() misses V \ (the_Vertices_of G2) or not W is trivial )
let V be set ; :: thesis: for G1 being addVertices of G2,V
for W being Walk of G1 holds
( W .vertices() misses V \ (the_Vertices_of G2) or not W is trivial )
let G1 be addVertices of G2,V; :: thesis: for W being Walk of G1 holds
( W .vertices() misses V \ (the_Vertices_of G2) or not W is trivial )
let W be Walk of G1; :: thesis: ( W .vertices() misses V \ (the_Vertices_of G2) or not W is trivial )
assume not W .vertices() misses V \ (the_Vertices_of G2) ; :: thesis: W is trivial
then (W .vertices()) /\ (V \ (the_Vertices_of G2)) <> {} by XBOOLE_0:def 7;
then consider v being object such that
A1: v in (W .vertices()) /\ (V \ (the_Vertices_of G2)) by XBOOLE_0:def 1;
( v in W .vertices() & v in V \ (the_Vertices_of G2) ) by A1, XBOOLE_0:def 4;
then A2: ( v in W .vertices() & v in V & not v in the_Vertices_of G2 ) by XBOOLE_0:def 5;
then consider n being odd Element of NAT such that
A3: ( n <= len W & W . n = v ) by GLIB_001:87;

per cases ( n < len W or n = len W ) by A3, XXREAL_0:1;

suppose n < len W ; :: thesis: W is trivial

per cases then ( W . (n + 1) DJoins W . n,W . (n + 2),G1 or W . (n + 1) DJoins W . (n + 2),W . n,G1 ) by GLIB_001:def 3, GLIB_000:16;

suppose W . (n + 1) DJoins W . n,W . (n + 2),G1 ; :: thesis: W is trivial

then W . (n + 1) DJoins W . n,W . (n + 2),G2 by Th89;
then ( W . (n + 1) in the_Edges_of G2 & (the_Source_of G2) . (W . (n + 1)) = W . n ) by GLIB_000:def 14;
hence W is trivial by A2, A3, FUNCT_2:5; :: thesis: verum

end;

suppose W . (n + 1) DJoins W . (n + 2),W . n,G1 ; :: thesis: W is trivial

then W . (n + 1) DJoins W . (n + 2),W . n,G2 by Th89;
then ( W . (n + 1) in the_Edges_of G2 & (the_Target_of G2) . (W . (n + 1)) = W . n ) by GLIB_000:def 14;
hence W is trivial by A2, A3, FUNCT_2:5; :: thesis: verum

end;

end;

end;

suppose A4: n = len W ; :: thesis: W is trivial

per cases ( n = 1 or n <> 1 ) ;

suppose n = 1 ; :: thesis: W is trivial

hence W is trivial by A4, GLIB_001:126; :: thesis: verum

end;

suppose n <> 1 ; :: thesis: W is trivial

then consider m being odd Nat such that
A5: m + 2 = n by CHORD:5;
reconsider m = m as odd Element of NAT by ORDINAL1:def 12;
m < len W by A4, A5, NAT_D:47;

per cases then ( W . (m + 1) DJoins W . m,W . (m + 2),G1 or W . (m + 1) DJoins W . (m + 2),W . m,G1 ) by GLIB_000:16, GLIB_001:def 3;

suppose W . (m + 1) DJoins W . m,W . (m + 2),G1 ; :: thesis: W is trivial

then W . (m + 1) DJoins W . m,W . (m + 2),G2 by Th89;
then ( W . (m + 1) in the_Edges_of G2 & (the_Target_of G2) . (W . (m + 1)) = W . (m + 2) ) by GLIB_000:def 14;
hence W is trivial by A2, A3, A5, FUNCT_2:5; :: thesis: verum

end;

suppose W . (m + 1) DJoins W . (m + 2),W . m,G1 ; :: thesis: W is trivial

then W . (m + 1) DJoins W . (m + 2),W . m,G2 by Th89;
then ( W . (m + 1) in the_Edges_of G2 & (the_Source_of G2) . (W . (m + 1)) = W . (m + 2) ) by GLIB_000:def 14;
hence W is trivial by A2, A3, A5, FUNCT_2:5; :: thesis: verum

end;

end;

end;

end;

end;

end;