theorem :: GLIB_001:59

for G being _Graph
for W being Walk of G
for n, m being Element of NAT holds
( (W .remove (m,n)) .first() = W .first() & (W .remove (m,n)) .last() = W .last() ) by Lm33;