let G be _Graph; for P being Path of G holds
( P .edges() misses G .loops() or ex v, e being object st
( e Joins v,v,G & P = G .walkOf (v,e,v) ) )
let P be Path of G; ( P .edges() misses G .loops() or ex v, e being object st
( e Joins v,v,G & P = G .walkOf (v,e,v) ) )
assume
P .edges() meets G .loops()
; ex v, e being object st
( e Joins v,v,G & P = G .walkOf (v,e,v) )
then
(P .edges()) /\ (G .loops()) <> {}
by XBOOLE_0:def 7;
then consider e being object such that
A1:
e in (P .edges()) /\ (G .loops())
by XBOOLE_0:def 1;
A2:
( e in P .edges() & e in G .loops() )
by A1, XBOOLE_0:def 4;
then consider v being object such that
A3:
e Joins v,v,G
by Def2;
consider v1, v2 being Vertex of G, n being odd Element of NAT such that
A4:
( n + 2 <= len P & v1 = P . n & e = P . (n + 1) & v2 = P . (n + 2) )
and
A5:
e Joins v1,v2,G
by A2, GLIB_001:103;
A6:
( v = v1 & v = v2 )
by A3, A5, GLIB_000:15;
then A7:
P . n = P . (n + 2)
by A4;
n + 0 < n + 2
by XREAL_1:8;
then A8:
( n = 1 & n + 2 = len P )
by A4, A7, GLIB_001:def 28;
then A9:
( P . 1 = v & P . (len P) = v )
by A4, A6;
take
v
; ex e being object st
( e Joins v,v,G & P = G .walkOf (v,e,v) )
take
e
; ( e Joins v,v,G & P = G .walkOf (v,e,v) )
thus
e Joins v,v,G
by A3; P = G .walkOf (v,e,v)
then
G .walkOf (v,e,v) = <*v,e,v*>
by GLIB_001:def 5;
hence
P = G .walkOf (v,e,v)
by A4, A8, A9, FINSEQ_1:45; verum