let G be _Graph; :: thesis: for W being Walk of G
for e being object st e in W .edges() & not e in G .loops() & W is Circuit-like holds
ex e0 being object st
( e0 in W .edges() & e0 <> e )
let W be Walk of G; :: thesis: for e being object st e in W .edges() & not e in G .loops() & W is Circuit-like holds
ex e0 being object st
( e0 in W .edges() & e0 <> e )
let e be object ; :: thesis: ( e in W .edges() & not e in G .loops() & W is Circuit-like implies ex e0 being object st
( e0 in W .edges() & e0 <> e ) )
assume A1: ( e in W .edges() & not e in G .loops() & W is Circuit-like ) ; :: thesis: ex e0 being object st
( e0 in W .edges() & e0 <> e )
then consider n being odd Element of NAT such that
A2: ( n < len W & W . (n + 1) = e ) by GLIB_001:100;
A3: len W > 3

proof

assume len W <= 3 ; :: thesis: contradiction
then (len W) + 0 <= 3 + 1 by XREAL_1:7;

per cases then ( len W = 1 or len W = 3 ) by CHORD:7;

suppose len W = 1 ; :: thesis: contradiction

then (2 * (W .length())) + 1 = (2 * 0) + 1 by GLIB_001:112;
hence contradiction by A1, GLIB_001:def 26; :: thesis: verum

end;

suppose len W = 3 ; :: thesis: contradiction

then (2 * (W .length())) + 1 = (2 * 1) + 1 by GLIB_001:112;
then consider e0 being object such that
A4: ( e0 Joins W .first() ,W .last() ,G & W = G .walkOf ((W .first()),e0,(W .last())) ) by Th28;
W .edges() = {e0} by A4, GLIB_001:108;
then A5: e = e0 by A1, TARSKI:def 1;
W .first() = W .last() by A1, GLIB_001:def 24;
hence contradiction by A1, A4, A5, GLIB_009:def 2; :: thesis: verum

end;

end;

end;

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

suppose A6: n = 1 ; :: thesis: ex e0 being object st
( e0 in W .edges() & e0 <> e )

reconsider m = n + 2 as odd Element of NAT ;
take W . (m + 1) ; :: thesis: ( W . (m + 1) in W .edges() & W . (m + 1) <> e )
thus W . (m + 1) in W .edges() by A3, A6, GLIB_001:100; :: thesis: W . (m + 1) <> e
m + 1 <= len W by A3, A6, NAT_1:13;
then W . (n + 1) <> W . (m + 1) by A1, A6, GLIB_001:138;
hence W . (m + 1) <> e by A2; :: thesis: verum

end;

suppose A7: n <> 1 ; :: thesis: ex e0 being object st
( e0 in W .edges() & e0 <> e )

reconsider m = 1 as odd Element of NAT by POLYFORM:4;
take W . (m + 1) ; :: thesis: ( W . (m + 1) in W .edges() & W . (m + 1) <> e )
m < len W by A3, XXREAL_0:2;
hence W . (m + 1) in W .edges() by GLIB_001:100; :: thesis: W . (m + 1) <> e
1 <= n by CHORD:2;
then m < n by A7, XXREAL_0:1;
then A8: m + 1 < n + 1 by XREAL_1:6;
n + 1 < (len W) + 1 by A2, XREAL_1:6;
then n + 1 <= len W by NAT_1:13;
then W . (n + 1) <> W . (m + 1) by A1, A8, GLIB_001:138;
hence W . (m + 1) <> e by A2; :: thesis: verum

end;

end;