let G2 be _Graph; :: thesis:
let V be set ; :: thesis:
let G1 be addLoops of G2,V; :: thesis:
let P be Path of G1; :: thesis:
A1: G2 is Subgraph of G1 by GLIB_006:57;

suppose ( P is trivial & P .edges() c= the_Edges_of G2 ) ; :: thesis:

hence ( P is Path of G2 or ex v, e being object st
( e Joins v,v,G1 & P = G1 .walkOf (v,e,v) ) ) by A1, GLIB_001:169, GLIB_001:176; :: thesis:

end;

suppose A2: P is trivial ; :: thesis:

P .first() in the_Vertices_of G1 ;
then P .first() in the_Vertices_of G2 by Th15;
hence ( P is Path of G2 or ex v, e being object st
( e Joins v,v,G1 & P = G1 .walkOf (v,e,v) ) ) by A1, A2, GLIB_001:168; :: thesis:

end;

suppose not V c= the_Vertices_of G2 ; :: thesis:

then G1 == G2 by Def5;
hence ( P is Path of G2 or ex v, e being object st
( e Joins v,v,G1 & P = G1 .walkOf (v,e,v) ) ) by GLIB_001:179, GLIB_001:181; :: thesis:

end;

suppose A3: ( not P .edges() c= the_Edges_of G2 & V c= the_Vertices_of G2 ) ; :: thesis:

then (P .edges()) \ (the_Edges_of G2) <> {} by XBOOLE_1:37;
then consider e being object such that
A4: e in (P .edges()) \ (the_Edges_of G2) by XBOOLE_0:def 1;
consider E being set , f being one-to-one Function such that
A5: ( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & dom f = E & rng f = V & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f ) by A3, Def5;
A6: ( not e in the_Edges_of G2 & e in the_Edges_of G1 ) by A4, XBOOLE_0:def 5;
then e in dom f by A5, XBOOLE_0:def 3;
then ( (the_Source_of G1) . e = f . e & (the_Target_of G1) . e = f . e ) by A5, FUNCT_4:13;
then A7: e Joins f . e,f . e,G1 by A6, GLIB_000:def 13;
e in P .edges() by A4, XBOOLE_0:def 5;
then consider n being odd Element of NAT such that
A8: ( n < len P & P . (n + 1) = e ) by GLIB_001:100;
P . (n + 1) Joins P . n,P . (n + 2),G1 by A8, GLIB_001:def 3;
then A9: ( P . n = f . e & P . (n + 2) = f . e ) by A7, A8, GLIB_000:15;
( n + 0 < n + 2 & n + 2 <= len P ) by A8, CHORD:4, XREAL_1:8;
then A10: ( n = 1 & n + 2 = len P ) by A9, GLIB_001:def 28;
A11: P = <*(f . e),e,(f . e)*> by A8, A9, A10, FINSEQ_1:45;

reconsider e = e as object ;
reconsider v = f . e as object ;
take v = v; :: thesis:
take e = e; :: thesis:
thus e Joins v,v,G1 by A7; :: thesis:
hence P = G1 .walkOf (v,e,v) by A11, GLIB_001:def 5; :: thesis:

end;

hence ( P is Path of G2 or ex v, e being object st
( e Joins v,v,G1 & P = G1 .walkOf (v,e,v) ) ) ; :: thesis:

end;

end;