let G be _Graph; :: thesis: for P being Path of G st P is open & len P > 3 holds
for e being object st e Joins P .last() ,P .first() ,G holds
P .addEdge e is Cycle-like
let W be Path of G; :: thesis: ( W is open & len W > 3 implies for e being object st e Joins W .last() ,W .first() ,G holds
W .addEdge e is Cycle-like )
assume that
A1: W is open and
A2: len W > 3 ; :: thesis: for e being object st e Joins W .last() ,W .first() ,G holds
W .addEdge e is Cycle-like
let e be object ; :: 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

A4: now :: thesis: not e in W .edges()

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

per cases ( ( v1 = W .first() & v2 = W .last() ) or ( v1 = W .last() & v2 = W .first() ) ) by A3, A8;

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

now :: thesis: not 1 <> n

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

end;

hence contradiction by A1, A2, A7, A10, GLIB_001:147; :: thesis: verum

end;

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

hence contradiction by A1, A6, A9, GLIB_001:147; :: thesis: verum

end;

end;

end;

set P = W .addEdge e;
A12: (W .addEdge e) .last() = W .first() by A3, GLIB_001:63;
A13: len (W .addEdge e) = (len W) + (2 * 1) by A3, GLIB_001:64;

A14: now :: thesis: for m, n being odd Element of NAT st m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n holds
( m = 1 & n = len (W .addEdge e) )

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 that
A15: m < n and
A16: n <= len (W .addEdge e) ; :: thesis: ( (W .addEdge e) . m = (W .addEdge e) . n implies ( m = 1 & n = len (W .addEdge e) ) )
m < (len W) + (2 * 1) by A13, A15, A16, XXREAL_0:2;
then A17: m <= ((len W) + 2) - 2 by Th3;
assume A18: (W .addEdge e) . m = (W .addEdge e) . n ; :: thesis: ( m = 1 & n = len (W .addEdge e) )
1 <= m by Th2;
then A19: m in dom W by A17, FINSEQ_3:25;
then A20: W . m = (W .addEdge e) . m by A3, GLIB_001:65;

A21: now :: thesis: not n < len (W .addEdge e)

assume n < len (W .addEdge e) ; :: thesis: contradiction
then n < (len W) + (2 * 1) by A3, GLIB_001:64;
then A22: n <= ((len W) + 2) - 2 by Th3;
1 <= n by Th2;
then A23: n in dom W by A22, FINSEQ_3:25;
W . n <> W . m by A1, A15, A22, GLIB_001:147;
hence contradiction by A3, A18, A20, A23, GLIB_001:65; :: thesis: verum

end;

then A24: (W .addEdge e) . n = W . 1 by A12, A16, XXREAL_0:1;

now :: thesis: not m <> 1

assume A25: m <> 1 ; :: thesis: contradiction
1 <= m by Th2;
then (2 * 0) + 1 < m by A25, XXREAL_0:1;
then W . 1 <> W . m by A1, A17, GLIB_001:147;
hence contradiction by A3, A18, A19, A24, GLIB_001:65; :: thesis: verum

end;

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

end;

e in (W .last()) .edgesInOut() by A3, GLIB_000:62;
then W .addEdge e is Trail-like by A4, GLIB_001:142;
then A26: W .addEdge e is Path-like by A14;
(W .addEdge e) .first() = W .first() by A3, GLIB_001:63;
then A27: W .addEdge e is closed by A12;
W .addEdge e is trivial by A3, GLIB_001:132;
hence W .addEdge e is Cycle-like by A27, A26; :: thesis: verum