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 V5() implies not W2 is V5() ) & ( 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 V5() implies not W2 is V5() ) & ( W1 is closed implies W2 is closed ) )

let W2 be Walk of G2; :: thesis: ( W1 .vertexSeq() = W2 .vertexSeq() implies ( ( W1 is V5() implies not W2 is V5() ) & ( W1 is closed implies W2 is closed ) ) )

assume A1: W1 .vertexSeq() = W2 .vertexSeq() ; :: thesis: ( ( W1 is V5() implies not W2 is V5() ) & ( W1 is closed implies W2 is closed ) )

for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds

( ( W1 is V5() implies not W2 is V5() ) & ( 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 V5() implies not W2 is V5() ) & ( W1 is closed implies W2 is closed ) )

let W2 be Walk of G2; :: thesis: ( W1 .vertexSeq() = W2 .vertexSeq() implies ( ( W1 is V5() implies not W2 is V5() ) & ( W1 is closed implies W2 is closed ) ) )

assume A1: W1 .vertexSeq() = W2 .vertexSeq() ; :: thesis: ( ( W1 is V5() implies not W2 is V5() ) & ( W1 is closed implies W2 is closed ) )

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

assume
W1 is V5()
; :: thesis: W2 is V5()

then W1 .length() <> 0 by GLIB_001:def 26;

then W2 .length() <> 0 by A1, Th30;

hence W2 is V5() by GLIB_001:def 26; :: thesis: verum

end;then W1 .length() <> 0 by GLIB_001:def 26;

then W2 .length() <> 0 by A1, Th30;

hence W2 is V5() by GLIB_001:def 26; :: thesis: verum