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 A1: ( not e in W .edges() & e in (W .last() ) .edgesInOut() ) ; :: thesis: W .addEdge e is Path-like
then A2: e Joins W .last() ,(W .last() ) .adj e,G by GLIB_000:70;
set v = (W .last() ) .adj e;
set W2 = W .addEdge e;
A3: W .addEdge e is Trail-like by A1, GLIB_001:143;
A4: len (W .addEdge e) = (len W) + 2 by A2, GLIB_001:65;

now

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

suppose A5: W is trivial ; :: 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:127;
hence W .addEdge e is Path-like by A1, A2, A5, GLIB_001:151; :: thesis: verum

end;

suppose A6: not W is trivial ; :: thesis: W .addEdge e is Path-like

A7: now

assume W is closed ; :: thesis: contradiction
then W is Cycle-like by A6, GLIB_001:def 31;
hence contradiction by Def2; :: thesis: verum

end;

now

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

now

assume A9: W . n = (W .last() ) .adj e ; :: thesis: contradiction
set W3 = (W .addEdge e) .cut n,(len (W .addEdge e));
A10: n <= len (W .addEdge e) by A4, A8, NAT_1:12;
A11: (W .addEdge e) .cut n,(len (W .addEdge e)) is Trail-like by A3;
A12: ( ((W .addEdge e) .cut n,(len (W .addEdge e))) .first() = (W .addEdge e) . n & ((W .addEdge e) .cut n,(len (W .addEdge e))) .last() = (W .addEdge e) . (len (W .addEdge e)) ) by A10, GLIB_001:38;
n in dom W by A8, FINSEQ_3:27;
then A13: ((W .addEdge e) .cut n,(len (W .addEdge e))) .first() = (W .last() ) .adj e by A2, A9, A12, GLIB_001:66;
A14: ((W .addEdge e) .cut n,(len (W .addEdge e))) .last() = (W .addEdge e) .last() by A12, GLIB_001:def 7
.= (W .last() ) .adj e by A2, GLIB_001:64 ;

now

assume (W .addEdge e) .cut n,(len (W .addEdge e)) is trivial ; :: thesis: contradiction
then len ((W .addEdge e) .cut n,(len (W .addEdge e))) = 1 by GLIB_001:127;
then 1 + n = (len (W .addEdge e)) + 1 by A10, GLIB_001:37;
then (2 + (len W)) - (len W) <= (len W) - (len W) by A4, A8, XREAL_1:15;
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
A15: not W4 is trivial by A11, GLIB_001:167;
W4 is_Walk_from (W .last() ) .adj e,(W .last() ) .adj e by A13, A14, GLIB_001:def 32;
then W4 is closed by GLIB_001:120;
then W4 is Cycle-like by A15, GLIB_001:def 31;
hence contradiction by Def2; :: thesis: verum

end;

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

end;

hence W .addEdge e is Path-like by A1, A2, A7, GLIB_001:151; :: thesis: verum

end;

end;

end;

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