let G be _Graph; :: thesis: for P being Path of G st not P is closed & len P > 3 holds
for e being set st e Joins P .last() ,P .first() ,G holds
P .addEdge e is Cycle-like
let W be Path of G; :: thesis: ( not W is closed & len W > 3 implies for e being set st e Joins W .last() ,W .first() ,G holds
W .addEdge e is Cycle-like )
assume that
A1: not W is closed and
A2: len W > 3 ; :: thesis: for e being set st e Joins W .last() ,W .first() ,G holds
W .addEdge e is Cycle-like
let e be set ; :: thesis: ( e Joins W .last() ,W .first() ,G implies W .addEdge e is Cycle-like )
assume A3: e Joins W .last() ,W .first() ,G ; :: thesis: W .addEdge e is Cycle-like
set P = W .addEdge e;
A4: ( (W .addEdge e) .first() = W .first() & (W .addEdge e) .last() = W .first() ) by A3, GLIB_001:64;
then A5: W .addEdge e is closed by GLIB_001:def 24;
A6: len (W .addEdge e) = (len W) + (2 * 1) by A3, GLIB_001:65;
A7: e in (W .last() ) .edgesInOut() by A3, GLIB_000:65;

now

assume e in W .edges() ; :: thesis: contradiction
then consider v1, v2 being Vertex of G, n being odd Element of NAT such that
A8: ( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) ) and
A9: e Joins v1,v2,G by GLIB_001:104;
A10: n < len W by A8, XREAL_1:41;

per cases ( ( v1 = W .first() & v2 = W .last() ) or ( v1 = W .last() & v2 = W .first() ) ) by A3, A9, GLIB_000:18;

suppose A11: ( v1 = W .first() & v2 = W .last() ) ; :: thesis: contradiction

now

assume 1 <> n ; :: thesis: contradiction
then ( 1 <= n & 1 <> n ) by Th2;
then (2 * 0 ) + 1 < n by XXREAL_0:1;
hence contradiction by A1, A8, A10, A11, GLIB_001:148; :: thesis: verum

end;

hence contradiction by A1, A2, A8, A11, GLIB_001:148; :: thesis: verum

end;

suppose ( v1 = W .last() & v2 = W .first() ) ; :: thesis: contradiction

hence contradiction by A1, A8, A10, GLIB_001:148; :: thesis: verum

end;

end;

end;

then A12: W .addEdge e is Trail-like by A7, GLIB_001:143;

now

let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n implies ( m = 1 & n = len (W .addEdge e) ) )
assume A13: ( m < n & n <= len (W .addEdge e) ) ; :: thesis: ( (W .addEdge e) . m = (W .addEdge e) . n implies ( m = 1 & n = len (W .addEdge e) ) )
assume A14: (W .addEdge e) . m = (W .addEdge e) . n ; :: thesis: ( m = 1 & n = len (W .addEdge e) )
A15: 1 <= m by Th2;
m < (len W) + (2 * 1) by A6, A13, XXREAL_0:2;
then A16: m <= ((len W) + 2) - 2 by Th3;
then A17: m in dom W by A15, FINSEQ_3:27;
then A18: W . m = (W .addEdge e) . m by A3, GLIB_001:66;

A19: now

assume n < len (W .addEdge e) ; :: thesis: contradiction
then n < (len W) + (2 * 1) by A3, GLIB_001:65;
then A20: n <= ((len W) + 2) - 2 by Th3;
then A21: W . n <> W . m by A1, A13, GLIB_001:148;
1 <= n by Th2;
then n in dom W by A20, FINSEQ_3:27;
hence contradiction by A3, A14, A18, A21, GLIB_001:66; :: thesis: verum

end;

then A22: (W .addEdge e) . n = W . 1 by A4, A13, XXREAL_0:1;

now

assume m <> 1 ; :: thesis: contradiction
then ( m <> 1 & 1 <= m ) by Th2;
then (2 * 0 ) + 1 < m by XXREAL_0:1;
then W . 1 <> W . m by A1, A16, GLIB_001:148;
hence contradiction by A3, A14, A17, A22, GLIB_001:66; :: thesis: verum

end;

hence ( m = 1 & n = len (W .addEdge e) ) by A13, A19, XXREAL_0:1; :: thesis: verum

end;

then A23: W .addEdge e is Path-like by A12, GLIB_001:def 28;
not W .addEdge e is trivial by A3, GLIB_001:133;
hence W .addEdge e is Cycle-like by A5, A23, GLIB_001:def 31; :: thesis: verum