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:
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 ;
per cases ( ( v1 = W .first() & v2 = W .last() ) or ( v1 = W .last() & v2 = W .first() ) ) by A3, A8;
end;
end;
set P = W .addEdge e;
A12: (W .addEdge e) .last() = W .first() by ;
A13: len (W .addEdge e) = (len W) + (2 * 1) by ;
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 ;
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 ;
then A20: W . m = (W .addEdge e) . m by ;
A21: now :: thesis: not n < len (W .addEdge e)
assume n < len (W .addEdge e) ; :: thesis: contradiction
then n < (len W) + (2 * 1) by ;
then A22: n <= ((len W) + 2) - 2 by Th3;
1 <= n by Th2;
then A23: n in dom W by ;
W . n <> W . m by ;
hence contradiction by A3, A18, A20, A23, GLIB_001:65; :: thesis: verum
end;
then A24: (W .addEdge e) . n = W . 1 by ;
now :: thesis: not m <> 1
assume A25: m <> 1 ; :: thesis: contradiction
1 <= m by Th2;
then (2 * 0) + 1 < m by ;
then W . 1 <> W . m by ;
hence contradiction by A3, A18, A19, A24, GLIB_001:65; :: thesis: verum
end;
hence ( m = 1 & n = len (W .addEdge e) ) by ; :: thesis: verum
end;
e in () .edgesInOut() by ;
then W .addEdge e is Trail-like by ;
then A26: W .addEdge e is Path-like by A14;
(W .addEdge e) .first() = W .first() by ;
then A27: W .addEdge e is closed by A12;
not W .addEdge e is trivial by ;
hence W .addEdge e is Cycle-like by ; :: thesis: verum