let G be _Graph; :: thesis: for W1, W2 being Walk of G st W2 is trivial & W2 .edges() c= W1 .edges() holds
W2 .vertices() c= W1 .vertices()
let W1, W2 be Walk of G; :: thesis: ( W2 is trivial & W2 .edges() c= W1 .edges() implies W2 .vertices() c= W1 .vertices() )
assume that
A1: 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()

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;

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

per cases ( n = len W2 or n <> len W2 ) ;

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;

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;

end;

end;

hence v in W1 .vertices() ; :: thesis: verum

end;

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