let G be _Graph; :: thesis: for W1, W2 being Walk of G st not W2 is trivial & W2 .edges() c= W1 .edges() holds

W2 .vertices() c= W1 .vertices()

let W1, W2 be Walk of G; :: thesis: ( not W2 is trivial & W2 .edges() c= W1 .edges() implies W2 .vertices() c= W1 .vertices() )

assume that

A1: not W2 is trivial and

A2: W2 .edges() c= W1 .edges() ; :: thesis: W2 .vertices() c= W1 .vertices()

A3: 3 <= len W2 by A1, Lm54;

W2 .vertices() c= W1 .vertices()

let W1, W2 be Walk of G; :: thesis: ( not W2 is trivial & W2 .edges() c= W1 .edges() implies W2 .vertices() c= W1 .vertices() )

assume that

A1: not W2 is trivial and

A2: W2 .edges() c= W1 .edges() ; :: thesis: W2 .vertices() c= W1 .vertices()

A3: 3 <= len W2 by A1, Lm54;

now :: thesis: for v being object st v in W2 .vertices() holds

v in W1 .vertices()

hence
W2 .vertices() c= W1 .vertices()
by TARSKI:def 3; :: thesis: verumv in W1 .vertices()

let v be object ; :: thesis: ( v in W2 .vertices() implies v in W1 .vertices() )

assume v in W2 .vertices() ; :: thesis: v in W1 .vertices()

then consider n being odd Element of NAT such that

A4: n <= len W2 and

A5: W2 . n = v by Lm45;

end;assume v in W2 .vertices() ; :: thesis: v in W1 .vertices()

then consider n being odd Element of NAT such that

A4: n <= len W2 and

A5: W2 . n = v by Lm45;

now :: thesis: v in W1 .vertices() end;

hence
v in W1 .vertices()
; :: thesis: verumper cases
( n = len W2 or n <> len W2 )
;

end;

suppose
n = len W2
; :: thesis: v in W1 .vertices()

then
3 - 1 < n - 0
by A3, XREAL_1:15;

then reconsider n5 = n - (2 * 1) as odd Element of NAT by INT_1:5;

A6: 1 <= n5 + 1 by NAT_1:12;

n5 < n - 0 by XREAL_1:15;

then A7: n5 < len W2 by A4, XXREAL_0:2;

then A8: W2 . (n5 + 1) Joins W2 . n5,W2 . (n5 + 2),G by Def3;

n5 + 1 <= len W2 by A7, NAT_1:13;

then W2 . (n5 + 1) in W2 .edges() by A6, Lm46;

then consider m being even Element of NAT such that

A9: 1 <= m and

A10: m <= len W1 and

A11: W1 . m = W2 . (n5 + 1) by A2, Lm46;

reconsider maa1 = m - 1 as odd Element of NAT by A9, INT_1:5;

A12: maa1 < (len W1) - 0 by A10, XREAL_1:15;

then A13: W1 . (maa1 + 1) Joins W1 . maa1,W1 . (maa1 + 2),G by Def3;

A14: W1 . maa1 = W1 .vertexAt maa1 by A12, Def8;

A15: maa1 + 2 <= len W1 by A12, Th1;

then W1 . (maa1 + 2) = W1 .vertexAt (maa1 + 2) by Def8;

then ( v = W1 .vertexAt maa1 or v = W1 .vertexAt (maa1 + 2) ) by A5, A8, A11, A13, A14, GLIB_000:15;

hence v in W1 .vertices() by A12, A15, Th87; :: thesis: verum

end;then reconsider n5 = n - (2 * 1) as odd Element of NAT by INT_1:5;

A6: 1 <= n5 + 1 by NAT_1:12;

n5 < n - 0 by XREAL_1:15;

then A7: n5 < len W2 by A4, XXREAL_0:2;

then A8: W2 . (n5 + 1) Joins W2 . n5,W2 . (n5 + 2),G by Def3;

n5 + 1 <= len W2 by A7, NAT_1:13;

then W2 . (n5 + 1) in W2 .edges() by A6, Lm46;

then consider m being even Element of NAT such that

A9: 1 <= m and

A10: m <= len W1 and

A11: W1 . m = W2 . (n5 + 1) by A2, Lm46;

reconsider maa1 = m - 1 as odd Element of NAT by A9, INT_1:5;

A12: maa1 < (len W1) - 0 by A10, XREAL_1:15;

then A13: W1 . (maa1 + 1) Joins W1 . maa1,W1 . (maa1 + 2),G by Def3;

A14: W1 . maa1 = W1 .vertexAt maa1 by A12, Def8;

A15: maa1 + 2 <= len W1 by A12, Th1;

then W1 . (maa1 + 2) = W1 .vertexAt (maa1 + 2) by Def8;

then ( v = W1 .vertexAt maa1 or v = W1 .vertexAt (maa1 + 2) ) by A5, A8, A11, A13, A14, GLIB_000:15;

hence v in W1 .vertices() by A12, A15, Th87; :: thesis: verum

suppose
n <> len W2
; :: thesis: v in W1 .vertices()

then A16:
n < len W2
by A4, XXREAL_0:1;

then W2 . (n + 1) in W2 .edges() by Th98;

then consider m being even Element of NAT such that

A17: 1 <= m and

A18: m <= len W1 and

A19: W1 . m = W2 . (n + 1) by A2, Lm46;

A20: W1 . m Joins v,W2 . (n + 2),G by A5, A16, A19, Def3;

reconsider maa1 = m - 1 as odd Element of NAT by A17, INT_1:5;

A21: maa1 < (len W1) - 0 by A18, XREAL_1:15;

then A22: W1 . (maa1 + 1) Joins W1 . maa1,W1 . (maa1 + 2),G by Def3;

A23: W1 . maa1 = W1 .vertexAt maa1 by A21, Def8;

A24: maa1 + 2 <= len W1 by A21, Th1;

then W1 . (maa1 + 2) = W1 .vertexAt (maa1 + 2) by Def8;

then ( v = W1 .vertexAt maa1 or v = W1 .vertexAt (maa1 + 2) ) by A20, A22, A23, GLIB_000:15;

hence v in W1 .vertices() by A21, A24, Th87; :: thesis: verum

end;then W2 . (n + 1) in W2 .edges() by Th98;

then consider m being even Element of NAT such that

A17: 1 <= m and

A18: m <= len W1 and

A19: W1 . m = W2 . (n + 1) by A2, Lm46;

A20: W1 . m Joins v,W2 . (n + 2),G by A5, A16, A19, Def3;

reconsider maa1 = m - 1 as odd Element of NAT by A17, INT_1:5;

A21: maa1 < (len W1) - 0 by A18, XREAL_1:15;

then A22: W1 . (maa1 + 1) Joins W1 . maa1,W1 . (maa1 + 2),G by Def3;

A23: W1 . maa1 = W1 .vertexAt maa1 by A21, Def8;

A24: maa1 + 2 <= len W1 by A21, Th1;

then W1 . (maa1 + 2) = W1 .vertexAt (maa1 + 2) by Def8;

then ( v = W1 .vertexAt maa1 or v = W1 .vertexAt (maa1 + 2) ) by A20, A22, A23, GLIB_000:15;

hence v in W1 .vertices() by A21, A24, Th87; :: thesis: verum