let G be _Graph; :: thesis: 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; :: thesis: ( 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() ; :: thesis: ex v, e being object st
( e Joins v,v,G & P = G .walkOf (v,e,v) )

then (P .edges()) /\ () <> {} by XBOOLE_0:def 7;
then consider e being object such that
A1: e in () /\ () by XBOOLE_0:def 1;
A2: ( e in P .edges() & e in G .loops() ) by ;
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 ;
A6: ( v = v1 & v = v2 ) by ;
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 ;
then A9: ( P . 1 = v & P . (len P) = v ) by A4, A6;
take v ; :: thesis: ex e being object st
( e Joins v,v,G & P = G .walkOf (v,e,v) )

take e ; :: thesis: ( e Joins v,v,G & P = G .walkOf (v,e,v) )
thus e Joins v,v,G by A3; :: thesis: 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 ; :: thesis: verum