let G be acyclic _Graph; :: thesis: for W being Path of G
for e being set st not e in W .edges() & e in () .edgesInOut() holds

let W be Path of G; :: thesis: for e being set st not e in W .edges() & e in () .edgesInOut() holds

let e be set ; :: thesis: ( not e in W .edges() & e in () .edgesInOut() implies W .addEdge e is Path-like )
assume that
A1: not e in W .edges() and
A2: e in () .edgesInOut() ; :: thesis:
set v = () .adj e;
set W2 = W .addEdge e;
A3: e Joins W .last() ,() .adj e,G by ;
then A4: len (W .addEdge e) = (len W) + 2 by GLIB_001:64;
A5: W .addEdge e is Trail-like by ;
now :: thesis:
per cases ( W is trivial or not W is trivial ) ;
suppose A7: not W is trivial ; :: thesis:
A8: now :: thesis: for n being odd Element of NAT st 1 < n & n <= len W holds
W . n <> () .adj e
let n be odd Element of NAT ; :: thesis: ( 1 < n & n <= len W implies W . n <> () .adj e )
assume that
A9: 1 < n and
A10: n <= len W ; :: thesis: W . n <> () .adj e
now :: thesis: not W . n = () .adj e
assume A11: W . n = () .adj e ; :: thesis: contradiction
A12: n <= len (W .addEdge e) by ;
then A13: ((W .addEdge e) .cut (n,(len (W .addEdge e)))) .first() = (W .addEdge e) . n by GLIB_001:37;
now :: thesis: not (W .addEdge e) .cut (n,(len (W .addEdge e))) is trivial
then len ((W .addEdge e) .cut (n,(len (W .addEdge e)))) = 1 by GLIB_001:126;
then 1 + n = (len (W .addEdge e)) + 1 by ;
then (2 + (len W)) - (len W) <= (len W) - (len W) by ;
then 2 <= 0 ;
hence contradiction ; :: thesis: verum
end;
then consider W4 being Path of (W .addEdge e) .cut (n,(len (W .addEdge e))) such that
A14: not W4 is trivial by ;
then A15: ((W .addEdge e) .cut (n,(len (W .addEdge e)))) .last() = (W .addEdge e) .last() by GLIB_001:def 7
.= () .adj e by ;
n in dom W by ;