let G be _Graph; :: thesis:
let C be Walk of G; :: thesis:
let u, v, w be object ; :: thesis:
assume that
A1: ( C is Cycle-like & u in C .vertices() & v in C .vertices() ) and
A2: ( u <> w & v <> w ) ; :: thesis:
consider n being odd Element of NAT such that
A3: ( n <= len C & C . n = u ) by A1, GLIB_001:87;
consider m being odd Element of NAT such that
A4: ( m <= len C & C . m = v ) by A1, GLIB_001:87;

per cases by A3, A4, XXREAL_0:1;

suppose A5: u = v ; :: thesis:

reconsider u9 = u as Vertex of G by A1;
reconsider W = G .walkOf u9 as Path of G ;
take W ; :: thesis:
thus W is_Walk_from u,v by A5, GLIB_001:13; :: thesis:
W .vertices() = {u} by GLIB_001:90;
hence not w in W .vertices() by A2, TARSKI:def 1; :: thesis:

end;

suppose A6: ( u <> v & n < m ) ; :: thesis:

per cases ;

suppose A7: not w in (C .cut (n,m)) .vertices() ; :: thesis:

reconsider W = C .cut (n,m) as Path of G by A1;
take W ; :: thesis:
thus ( W is_Walk_from u,v & not w in W .vertices() ) by A3, A4, A6, A7, GLIB_001:37; :: thesis:

end;

suppose w in (C .cut (n,m)) .vertices() ; :: thesis:

then consider k being odd Element of NAT such that
A8: ( k <= len (C .cut (n,m)) & (C .cut (n,m)) . k = w ) by GLIB_001:87;
reconsider k3 = k - 1 as even Nat by CHORD:2;
reconsider k3 = k3 as Element of NAT by ORDINAL1:def 12;
k < (len (C .cut (n,m))) + 1 by A8, NAT_1:13;
then A9: k3 < ((len (C .cut (n,m))) + 1) - 1 by XREAL_1:14;
A10: (C .cut (n,m)) . (k3 + 1) = C . (n + k3) by A4, A6, A9, GLIB_001:36;
reconsider W1 = C .cut (1,n), W2 = C .cut (m,(len C)) as Path of G by A1;
A11: ( 1 is odd & len C is odd ) by POLYFORM:4;
A12: 1 <= n by CHORD:2;
(len (C .cut (n,m))) + n = m + 1 by A4, A6, GLIB_001:36;
then A13: n + k3 < m + 1 by A9, XREAL_1:8;
A14: ( w in W1 .vertices() implies n + k3 = len C )

proof

assume w in W1 .vertices() ; :: thesis:
then consider k2 being odd Element of NAT such that
A15: ( k2 <= len W1 & W1 . k2 = w ) by GLIB_001:87;
reconsider k4 = k2 - 1 as Nat by CHORD:2;
reconsider k4 = k4 as Element of NAT by ORDINAL1:def 12;
k2 < (len W1) + 1 by A15, NAT_1:13;
then k4 < ((len W1) + 1) - 1 by XREAL_1:14;
then A16: W1 . (k4 + 1) = C . (1 + k4) by A3, A11, A12, GLIB_001:36;
then A17: C . (n + k3) = C . (1 + k4) by A8, A10, A15;
(len W1) + 1 = n + 1 by A3, A11, A12, GLIB_001:36;
then 1 + k4 <= n by A15;
then 1 + k4 < n by A2, A3, A15, A16, XXREAL_0:1;
then A19: (1 + k4) + 0 < n + k3 by XREAL_1:8;
n + k3 <= m by A13, NAT_1:13;
then n + k3 <= len C by A4, XXREAL_0:2;
hence n + k3 = len C by A1, A17, A19, GLIB_001:def 28; :: thesis:

end;

A20: ( w in W2 .vertices() implies n + k3 = 1 )

proof

assume w in W2 .vertices() ; :: thesis:
then consider k2 being odd Element of NAT such that
A21: ( k2 <= len W2 & W2 . k2 = w ) by GLIB_001:87;
reconsider k4 = k2 - 1 as Nat by CHORD:2;
reconsider k4 = k4 as Element of NAT by ORDINAL1:def 12;
k2 < (len W2) + 1 by A21, NAT_1:13;
then A22: k4 < ((len W2) + 1) - 1 by XREAL_1:14;
then A23: W2 . (k4 + 1) = C . (m + k4) by A4, GLIB_001:36;
then A24: C . (n + k3) = C . (m + k4) by A8, A10, A21;
1 < k4

proof

assume k4 <= 1 ; :: thesis:
then k4 = 0 by A11, NAT_1:25;
hence contradiction by A2, A4, A21, A23; :: thesis:

end;

then m + 1 < m + k4 by XREAL_1:8;
then A25: n + k3 < m + k4 by A13, XXREAL_0:2;
m + k4 < (len W2) + m by A22, XREAL_1:8;
then m + k4 < (len C) + 1 by A4, GLIB_001:36;
then m + k4 <= len C by NAT_1:13;
hence n + k3 = 1 by A1, A24, A25, GLIB_001:def 28; :: thesis:

end;

per cases ;

suppose ( n <> 1 & m <> len C ) ; :: thesis:

then A26: ( 1 < n & m < len C ) by A4, A12, XXREAL_0:1;
then A27: m <> 1 by A6;
A28: W2 .last() = C .last() by A4, GLIB_001:37
.= C .first() by A1, GLIB_001:def 24
.= W1 .first() by A3, A11, A12, GLIB_001:37 ;
A29: W1 is open by A1, A3, A6, A11, A26, Th30;
A30: W2 is open by A1, A26, A27, Th30;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in (W2 .vertices()) /\ (W1 .vertices()) ; :: thesis:
then A31: ( x in W2 .vertices() & x in W1 .vertices() ) by XBOOLE_0:def 4;
then consider n0 being odd Element of NAT such that
A32: ( n0 <= len W1 & W1 . n0 = x ) by GLIB_001:87;
consider m0 being odd Element of NAT such that
A33: ( m0 <= len W2 & W2 . m0 = x ) by A31, GLIB_001:87;
( 1 <= n0 & 1 <= m0 ) by CHORD:2;
then A34: ( n0 in dom W1 & m0 in dom W2 ) by A32, A33, FINSEQ_3:25;
A35: m0 - 1 >= 1 - 1 by CHORD:2, XREAL_1:9;
then 0 + m <= (m0 - 1) + m by XREAL_1:6;
then A36: n < (m + m0) - 1 by A6, XXREAL_0:2;
(len W1) + 1 = n + 1 by A3, A11, A12, GLIB_001:36;
then A37: n0 < (m + m0) - 1 by A32, A36, XXREAL_0:2;
reconsider m1 = m0 - 1 as Element of NAT by A35, INT_1:3;
m1 + 1 <= len W2 by A33;
then m1 < len W2 by NAT_1:13;
then m + m1 in dom C by A4, GLIB_001:36;
then A38: (m + m0) - 1 <= len C by FINSEQ_3:25;
A39: m + m1 is odd ;
C . n0 = C . ((1 + n0) - 1)
.= W2 . m0 by A3, A11, A12, A32, A33, A34, GLIB_001:47
.= C . ((m + m0) - 1) by A4, A34, GLIB_001:47 ;
then n0 = 1 by A1, A37, A38, A39, GLIB_001:def 28;
hence x = W2 .last() by A28, A32; :: thesis:

end;

assume x = W2 .last() ; :: thesis:
then ( x in W2 .vertices() & x in W1 .vertices() ) by A28, GLIB_001:88;
hence x in (W2 .vertices()) /\ (W1 .vertices()) by XBOOLE_0:def 4; :: thesis:

end;

then (W2 .vertices()) /\ (W1 .vertices()) = {(W2 .last())} by TARSKI:def 1;
then W2 .append W1 is Path of G by A28, A29, A30, HELLY:19;
then reconsider W = (W2 .append W1) .reverse() as Path of G ;
take W ; :: thesis:
W1 is_Walk_from C .first() ,C . n by A3, A11, A12, GLIB_001:37;
then A40: W1 is_Walk_from C .last() ,C . n by A1, GLIB_001:def 24;
A41: W2 is_Walk_from C . m,C .last() by A4, GLIB_001:37;
W2 .append W1 is_Walk_from C . m,C . n by A40, A41, GLIB_001:31;
hence W is_Walk_from u,v by A3, A4, GLIB_001:23; :: thesis:
thus not w in W .vertices() :: thesis:

proof

A42: W1 .first() = C .last() by A40, GLIB_001:def 23
.= W2 .last() by A41, GLIB_001:def 23 ;
assume w in W .vertices() ; :: thesis:
then w in (W2 .append W1) .vertices() by GLIB_001:92;
then w in (W2 .vertices()) \/ (W1 .vertices()) by A42, GLIB_001:93;

per cases by XBOOLE_0:def 3;

suppose w in W2 .vertices() ; :: thesis:

hence contradiction by A26, A20, XREAL_1:31; :: thesis:

end;

suppose w in W1 .vertices() ; :: thesis:

hence contradiction by A13, A14, A26, NAT_1:13; :: thesis:

end;

suppose A43: n = 1 ; :: thesis:

take W2 .reverse() ; :: thesis:
W2 is_Walk_from C . m,C .last() by A4, GLIB_001:37;
then W2 is_Walk_from C . m,C .first() by A1, GLIB_001:def 24;
hence W2 .reverse() is_Walk_from u,v by A3, A4, A43, GLIB_001:23; :: thesis:
thus not w in (W2 .reverse()) .vertices() by A2, A3, A20, A8, A10, A43, GLIB_001:92; :: thesis:

end;

suppose A44: m = len C ; :: thesis:

take W1 .reverse() ; :: thesis:
W1 is_Walk_from C . 1,C . n by A3, A11, A12, GLIB_001:37;
then W1 is_Walk_from C . m,C . n by A1, A44, GLIB_001:118;
hence W1 .reverse() is_Walk_from u,v by A3, A4, GLIB_001:23; :: thesis:
thus not w in (W1 .reverse()) .vertices() by A2, A4, A14, A8, A10, A44, GLIB_001:92; :: thesis:

end;

suppose A45: ( u <> v & m < n ) ; :: thesis:

per cases ;

suppose A46: not w in (C .cut (m,n)) .vertices() ; :: thesis:

reconsider W = C .cut (m,n) as Path of G by A1;
take W .reverse() ; :: thesis:
thus ( W .reverse() is_Walk_from u,v & not w in (W .reverse()) .vertices() ) by A3, A4, A45, A46, GLIB_001:23, GLIB_001:37, GLIB_001:92; :: thesis:

end;

suppose w in (C .cut (m,n)) .vertices() ; :: thesis:

then consider k being odd Element of NAT such that
A47: ( k <= len (C .cut (m,n)) & (C .cut (m,n)) . k = w ) by GLIB_001:87;
reconsider k3 = k - 1 as even Nat by CHORD:2;
reconsider k3 = k3 as Element of NAT by ORDINAL1:def 12;
k < (len (C .cut (m,n))) + 1 by A47, NAT_1:13;
then A48: k3 < ((len (C .cut (m,n))) + 1) - 1 by XREAL_1:14;
A49: (C .cut (m,n)) . (k3 + 1) = C . (m + k3) by A3, A45, A48, GLIB_001:36;
reconsider W1 = C .cut (1,m), W2 = C .cut (n,(len C)) as Path of G by A1;
A50: ( 1 is odd & len C is odd ) by POLYFORM:4;
A51: 1 <= m by CHORD:2;
(len (C .cut (m,n))) + m = n + 1 by A3, A45, GLIB_001:36;
then A52: m + k3 < n + 1 by A48, XREAL_1:8;
A53: ( w in W1 .vertices() implies m + k3 = len C )

proof

assume w in W1 .vertices() ; :: thesis:
then consider k2 being odd Element of NAT such that
A54: ( k2 <= len W1 & W1 . k2 = w ) by GLIB_001:87;
reconsider k4 = k2 - 1 as Nat by CHORD:2;
reconsider k4 = k4 as Element of NAT by ORDINAL1:def 12;
k2 < (len W1) + 1 by A54, NAT_1:13;
then k4 < ((len W1) + 1) - 1 by XREAL_1:14;
then A55: W1 . (k4 + 1) = C . (1 + k4) by A4, A50, A51, GLIB_001:36;
then A56: C . (m + k3) = C . (1 + k4) by A47, A49, A54;
(len W1) + 1 = m + 1 by A4, A50, A51, GLIB_001:36;
then 1 + k4 < m by A2, A4, A54, A55, XXREAL_0:1;
then A58: (1 + k4) + 0 < m + k3 by XREAL_1:8;
m + k3 <= n by A52, NAT_1:13;
then m + k3 <= len C by A3, XXREAL_0:2;
hence m + k3 = len C by A1, A56, A58, GLIB_001:def 28; :: thesis:

end;

A59: ( w in W2 .vertices() implies m + k3 = 1 )

proof

assume w in W2 .vertices() ; :: thesis:
then consider k2 being odd Element of NAT such that
A60: ( k2 <= len W2 & W2 . k2 = w ) by GLIB_001:87;
reconsider k4 = k2 - 1 as Nat by CHORD:2;
reconsider k4 = k4 as Element of NAT by ORDINAL1:def 12;
k2 < (len W2) + 1 by A60, NAT_1:13;
then A61: k4 < ((len W2) + 1) - 1 by XREAL_1:14;
then A62: W2 . (k4 + 1) = C . (n + k4) by A3, GLIB_001:36;
then A63: C . (m + k3) = C . (n + k4) by A47, A49, A60;
1 < k4

proof

assume k4 <= 1 ; :: thesis:
then k4 = 0 by A50, NAT_1:25;
hence contradiction by A2, A3, A60, A62; :: thesis:

end;

then n + 1 < n + k4 by XREAL_1:8;
then A64: m + k3 < n + k4 by A52, XXREAL_0:2;
n + k4 < (len W2) + n by A61, XREAL_1:8;
then n + k4 < (len C) + 1 by A3, GLIB_001:36;
then n + k4 <= len C by NAT_1:13;
hence m + k3 = 1 by A1, A63, A64, GLIB_001:def 28; :: thesis:

end;

per cases ;

suppose ( m <> 1 & n <> len C ) ; :: thesis:

then A65: ( 1 < m & n < len C ) by A3, A51, XXREAL_0:1;
then A66: n <> 1 by A45;
A67: W2 .last() = C .last() by A3, GLIB_001:37
.= C .first() by A1, GLIB_001:def 24
.= W1 .first() by A4, A50, A51, GLIB_001:37 ;
A68: W1 is open by A1, A4, A45, A50, A65, Th30;
A69: W2 is open by A1, A65, A66, Th30;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in (W2 .vertices()) /\ (W1 .vertices()) ; :: thesis:
then A70: ( x in W2 .vertices() & x in W1 .vertices() ) by XBOOLE_0:def 4;
then consider n0 being odd Element of NAT such that
A71: ( n0 <= len W1 & W1 . n0 = x ) by GLIB_001:87;
consider m0 being odd Element of NAT such that
A72: ( m0 <= len W2 & W2 . m0 = x ) by A70, GLIB_001:87;
( 1 <= n0 & 1 <= m0 ) by CHORD:2;
then A73: ( n0 in dom W1 & m0 in dom W2 ) by A71, A72, FINSEQ_3:25;
A74: m0 - 1 >= 1 - 1 by CHORD:2, XREAL_1:9;
then 0 + n <= (m0 - 1) + n by XREAL_1:6;
then A75: m < (n + m0) - 1 by A45, XXREAL_0:2;
(len W1) + 1 = m + 1 by A4, A50, A51, GLIB_001:36;
then A76: n0 < (n + m0) - 1 by A71, A75, XXREAL_0:2;
reconsider m1 = m0 - 1 as Element of NAT by A74, INT_1:3;
m1 + 1 <= len W2 by A72;
then m1 < len W2 by NAT_1:13;
then n + m1 in dom C by A3, GLIB_001:36;
then A77: (n + m0) - 1 <= len C by FINSEQ_3:25;
A78: n + m1 is odd ;
C . n0 = C . ((1 + n0) - 1)
.= W2 . m0 by A4, A50, A51, A71, A72, A73, GLIB_001:47
.= C . ((n + m0) - 1) by A3, A73, GLIB_001:47 ;
then n0 = 1 by A1, A76, A77, A78, GLIB_001:def 28;
hence x = W2 .last() by A67, A71; :: thesis:

end;

assume x = W2 .last() ; :: thesis:
then ( x in W2 .vertices() & x in W1 .vertices() ) by A67, GLIB_001:88;
hence x in (W2 .vertices()) /\ (W1 .vertices()) by XBOOLE_0:def 4; :: thesis:

end;

then (W2 .vertices()) /\ (W1 .vertices()) = {(W2 .last())} by TARSKI:def 1;
then reconsider W = W2 .append W1 as Path of G by A67, A68, A69, HELLY:19;
take W ; :: thesis:
W1 is_Walk_from C .first() ,C . m by A4, A50, A51, GLIB_001:37;
then A79: W1 is_Walk_from C .last() ,C . m by A1, GLIB_001:def 24;
A80: W2 is_Walk_from C . n,C .last() by A3, GLIB_001:37;
W2 .append W1 is_Walk_from C . n,C . m by A79, A80, GLIB_001:31;
hence W is_Walk_from u,v by A3, A4; :: thesis:
thus not w in W .vertices() :: thesis:

proof

A81: W1 .first() = C .last() by A79, GLIB_001:def 23
.= W2 .last() by A80, GLIB_001:def 23 ;
assume w in W .vertices() ; :: thesis:
then w in (W2 .vertices()) \/ (W1 .vertices()) by A81, GLIB_001:93;

per cases by XBOOLE_0:def 3;

suppose w in W2 .vertices() ; :: thesis:

hence contradiction by A65, A59, XREAL_1:31; :: thesis:

end;

suppose w in W1 .vertices() ; :: thesis:

hence contradiction by A52, A53, A65, NAT_1:13; :: thesis:

end;

suppose A82: m = 1 ; :: thesis:

take W2 ; :: thesis:
W2 is_Walk_from C . n,C .last() by A3, GLIB_001:37;
then W2 is_Walk_from C . n,C .first() by A1, GLIB_001:def 24;
hence W2 is_Walk_from u,v by A3, A4, A82; :: thesis:
thus not w in W2 .vertices() by A2, A4, A59, A47, A49, A82; :: thesis:

end;

suppose A83: n = len C ; :: thesis:

take W1 ; :: thesis:
W1 is_Walk_from C . 1,C . m by A4, A50, A51, GLIB_001:37;
hence W1 is_Walk_from u,v by A1, A3, A4, A83, GLIB_001:118; :: thesis:
thus not w in W1 .vertices() by A2, A3, A53, A47, A49, A83; :: thesis:

end;