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()) /\ (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 ; :: 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 A4, A8, A9, FINSEQ_1:45; :: thesis: verum

( 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()) /\ (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 ; :: 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 A4, A8, A9, FINSEQ_1:45; :: thesis: verum