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

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;

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;

not W .addEdge e is trivial by A3, GLIB_001:132;

hence W .addEdge e is Cycle-like by A27, A26; :: thesis: verum

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()

set P = W .addEdge e;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;

end;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;

end;

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

end;

now :: thesis: not 1 <> n

hence
contradiction
by A1, A2, A7, A10, GLIB_001:147; :: thesis: verumassume 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;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

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) )

e in (W .last()) .edgesInOut()
by A3, GLIB_000:62;( 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;

end;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)

then A24:
(W .addEdge e) . n = W . 1
by A12, A16, XXREAL_0:1;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 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

now :: thesis: not m <> 1

hence
( m = 1 & n = len (W .addEdge e) )
by A16, A21, XXREAL_0:1; :: thesis: verumassume 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;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

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;

not W .addEdge e is trivial by A3, GLIB_001:132;

hence W .addEdge e is Cycle-like by A27, A26; :: thesis: verum