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:
A3: 3 <= len W2 by ;
now :: thesis: for v being object st v in W2 .vertices() holds
v in W1 .vertices()
let v be object ; :: thesis: ( v in W2 .vertices() implies v in W1 .vertices() )
assume v in W2 .vertices() ; :: thesis:
then consider n being odd Element of NAT such that
A4: n <= len W2 and
A5: W2 . n = v by Lm45;
now :: thesis:
per cases ( n = len W2 or n <> len W2 ) ;
suppose n = len W2 ; :: thesis:
then 3 - 1 < n - 0 by ;
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 ;
then A8: W2 . (n5 + 1) Joins W2 . n5,W2 . (n5 + 2),G by Def3;
n5 + 1 <= len W2 by ;
then W2 . (n5 + 1) in W2 .edges() by ;
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 ;
reconsider maa1 = m - 1 as odd Element of NAT by ;
A12: maa1 < (len W1) - 0 by ;
then A13: W1 . (maa1 + 1) Joins W1 . maa1,W1 . (maa1 + 2),G by Def3;
A14: W1 . maa1 = W1 .vertexAt maa1 by ;
A15: maa1 + 2 <= len W1 by ;
then W1 . (maa1 + 2) = W1 .vertexAt (maa1 + 2) by Def8;
then ( v = W1 .vertexAt maa1 or v = W1 .vertexAt (maa1 + 2) ) by ;
hence v in W1 .vertices() by ; :: thesis: verum
end;
suppose n <> len W2 ; :: thesis:
then A16: n < len W2 by ;
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 ;
A20: W1 . m Joins v,W2 . (n + 2),G by A5, A16, A19, Def3;
reconsider maa1 = m - 1 as odd Element of NAT by ;
A21: maa1 < (len W1) - 0 by ;
then A22: W1 . (maa1 + 1) Joins W1 . maa1,W1 . (maa1 + 2),G by Def3;
A23: W1 . maa1 = W1 .vertexAt maa1 by ;
A24: maa1 + 2 <= len W1 by ;
then W1 . (maa1 + 2) = W1 .vertexAt (maa1 + 2) by Def8;
then ( v = W1 .vertexAt maa1 or v = W1 .vertexAt (maa1 + 2) ) by ;
hence v in W1 .vertices() by ; :: thesis: verum
end;
end;
end;
hence v in W1 .vertices() ; :: thesis: verum
end;
hence W2 .vertices() c= W1 .vertices() by TARSKI:def 3; :: thesis: verum