let G be _Graph; :: thesis: for W being Walk of G
for m, n being Element of NAT holds
( (W .remove (m,n)) .first() = W .first() & (W .remove (m,n)) .last() = W .last() )
let W be Walk of G; :: thesis: for m, n being Element of NAT holds
( (W .remove (m,n)) .first() = W .first() & (W .remove (m,n)) .last() = W .last() )
let m, n be Element of NAT ; :: thesis: ( (W .remove (m,n)) .first() = W .first() & (W .remove (m,n)) .last() = W .last() )
W is_Walk_from W .first() ,W .last() ;
then W .remove (m,n) is_Walk_from W .first() ,W .last() by Lm25;
hence ( (W .remove (m,n)) .first() = W .first() & (W .remove (m,n)) .last() = W .last() ) ; :: thesis: verum