let G be acyclic _Graph; :: thesis: for W being Path of G
for e being set st not e in W .edges() & e in (W .last()) .edgesInOut() holds
W .addEdge e is Path-like
let W be Path of G; :: thesis: for e being set st not e in W .edges() & e in (W .last()) .edgesInOut() holds
W .addEdge e is Path-like
let e be set ; :: thesis: ( not e in W .edges() & e in (W .last()) .edgesInOut() implies W .addEdge e is Path-like )
assume that
A1: not e in W .edges() and
A2: e in (W .last()) .edgesInOut() ; :: thesis: W .addEdge e is Path-like
set v = (W .last()) .adj e;
set W2 = W .addEdge e;
A3: e Joins W .last() ,(W .last()) .adj e,G by A2, GLIB_000:67;
then A4: len (W .addEdge e) = (len W) + 2 by GLIB_001:64;
A5: W .addEdge e is Trail-like by A1, A2, GLIB_001:142;

now :: thesis: W .addEdge e is Path-like

per cases ( not W is V5() or not W is V5() ) ;

suppose A6: W is V5() ; :: thesis: W .addEdge e is Path-like

then for n being odd Element of NAT st 1 < n & n <= len W holds
W . n <> (W .last()) .adj e by GLIB_001:126;
hence W .addEdge e is Path-like by A1, A3, A6, GLIB_001:150; :: thesis: verum

end;

suppose A7: W is V5() ; :: thesis: W .addEdge e is Path-like

A8: now :: thesis: for n being odd Element of NAT st 1 < n & n <= len W holds
W . n <> (W .last()) .adj e

let n be odd Element of NAT ; :: thesis: ( 1 < n & n <= len W implies W . n <> (W .last()) .adj e )
assume that
A9: 1 < n and
A10: n <= len W ; :: thesis: W . n <> (W .last()) .adj e

now :: thesis: not W . n = (W .last()) .adj e

set W3 = (W .addEdge e) .cut (n,(len (W .addEdge e)));
assume A11: W . n = (W .last()) .adj e ; :: thesis: contradiction
A12: n <= len (W .addEdge e) by A4, A10, NAT_1:12;
then A13: ((W .addEdge e) .cut (n,(len (W .addEdge e)))) .first() = (W .addEdge e) . n by GLIB_001:37;

now :: thesis: (W .addEdge e) .cut (n,(len (W .addEdge e))) is V5()

assume (W .addEdge e) .cut (n,(len (W .addEdge e))) is V5() ; :: thesis: contradiction
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 A12, GLIB_001:36;
then (2 + (len W)) - (len W) <= (len W) - (len W) by A4, A10, XREAL_1:13;
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: W4 is V5() by A5, GLIB_001:166;
((W .addEdge e) .cut (n,(len (W .addEdge e)))) .last() = (W .addEdge e) . (len (W .addEdge e)) by A12, GLIB_001:37;
then A15: ((W .addEdge e) .cut (n,(len (W .addEdge e)))) .last() = (W .addEdge e) .last() by GLIB_001:def 7
.= (W .last()) .adj e by A3, GLIB_001:63 ;
n in dom W by A9, A10, FINSEQ_3:25;
then ((W .addEdge e) .cut (n,(len (W .addEdge e)))) .first() = (W .last()) .adj e by A3, A11, A13, GLIB_001:65;
then W4 is_Walk_from (W .last()) .adj e,(W .last()) .adj e by A15, GLIB_001:def 32;
then W4 is closed by GLIB_001:119;
then W4 is Cycle-like by A14, GLIB_001:def 31;
hence contradiction by Def2; :: thesis: verum

end;

hence W . n <> (W .last()) .adj e ; :: thesis: verum

end;

not W is closed by A7, GLIB_001:def 31, Def2;
hence W .addEdge e is Path-like by A1, A3, A8, GLIB_001:150; :: thesis: verum

end;

end;

end;

hence W .addEdge e is Path-like ; :: thesis: verum