let G be _Graph; :: thesis:
let W be Walk of G; :: thesis:
given m, n being odd Nat such that A1: m + 2 < n and
A2: n <= len W and
A3: W . m <> W . n and
A4: ex e being object st e Joins W . m,W . n,G and
A5: for f being object st f in W .edges() holds
not f Joins W . m,W . n,G ; :: according to CHORD:def 10 :: thesis:
take m ; :: thesis:
take n ; :: thesis:
thus m + 2 < n by A1; :: thesis:
thus n <= len W by A2; :: thesis:
thus W . m <> W . n by A3; :: thesis:
thus ex e being object st e Joins W . m,W . n,G by A4; :: thesis:
A6: W .last() = W . (len W) ;
assume A7: W is Cycle-like ; :: thesis:
then A8: 3 <= len W by GLIB_001:125;
then reconsider lW2 = (len W) - (2 * 1) as odd Element of NAT by INT_1:5, XXREAL_0:2;
A9: W .first() = W . 1 ;
then A10: W . 1 = W . (len W) by A7, A6, GLIB_001:def 24;
reconsider lW2 = lW2 as odd Nat ;
reconsider le = lW2 + 1 as even Nat ;
A11: 1 <= le by NAT_1:12;
A12: lW2 < len W by XREAL_1:44;
then A13: le <= len W by NAT_1:13;
then le div 2 in dom (W .edgeSeq()) by A11, GLIB_001:77;
then (W .edgeSeq()) . (le div 2) in rng (W .edgeSeq()) by FUNCT_1:3;
then A14: W . (((len W) - 2) + 1) in W .edges() by A11, A13, GLIB_001:77;
thus ( not m = 1 or not n = len W ) by A3, A7, A9, A6, GLIB_001:def 24; :: thesis:
W . (lW2 + 1) Joins W . lW2,W . (lW2 + 2),G by A12, GLIB_001:def 3;
hence ( not m = 1 or not n = (len W) - 2 ) by A5, A10, A14, GLIB_000:14; :: thesis:
A15: (2 * 0) + 1 is odd Nat ;
A16: (2 * 1) div 2 = 1 by NAT_D:18;
A17: 1 + 1 <= len W by A8, XXREAL_0:2;
then 1 in dom (W .edgeSeq()) by A16, GLIB_001:77;
then (W .edgeSeq()) . 1 in rng (W .edgeSeq()) by FUNCT_1:3;
then A18: W . (1 + 1) in rng (W .edgeSeq()) by A16, A17, GLIB_001:77;
1 < len W by A8, XXREAL_0:2;
then W . (1 + 1) Joins W . 1,W . (1 + 2),G by A15, GLIB_001:def 3;
hence ( not m = 3 or not n = len W ) by A5, A10, A18, GLIB_000:14; :: thesis: