let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds
( ( W1 is trivial implies not W2 is trivial ) & ( W1 is closed implies W2 is closed ) )
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds
( ( W1 is trivial implies not W2 is trivial ) & ( W1 is closed implies W2 is closed ) )
let W2 be Walk of G2; :: thesis: ( W1 .vertexSeq() = W2 .vertexSeq() implies ( ( W1 is trivial implies not W2 is trivial ) & ( W1 is closed implies W2 is closed ) ) )
assume A1: W1 .vertexSeq() = W2 .vertexSeq() ; :: thesis: ( ( W1 is trivial implies not W2 is trivial ) & ( W1 is closed implies W2 is closed ) )

hereby :: thesis: ( W1 is closed implies W2 is closed )

assume W1 is trivial ; :: thesis: W2 is trivial
then W1 .length() <> 0 by GLIB_001:def 26;
then W2 .length() <> 0 by A1, Th30;
hence W2 is trivial by GLIB_001:def 26; :: thesis: verum

end;

hereby :: thesis: verum

assume W1 is closed ; :: thesis: W2 is closed
then W1 .first() = W1 .last() by GLIB_001:def 24;
then W1 .first() = W2 .last() by A1, Th30;
then W2 .first() = W2 .last() by A1, Th30;
hence W2 is closed by GLIB_001:def 24; :: thesis: verum

end;