let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 is Subwalk of W2 holds
( W1 .first() = W2 .first() & W1 .last() = W2 .last() )
let W1, W2 be Walk of G; :: thesis: ( W1 is Subwalk of W2 implies ( W1 .first() = W2 .first() & W1 .last() = W2 .last() ) )
assume W1 is Subwalk of W2 ; :: thesis: ( W1 .first() = W2 .first() & W1 .last() = W2 .last() )
then W1 is_Walk_from W2 .first() ,W2 .last() by Def32;
hence ( W1 .first() = W2 .first() & W1 .last() = W2 .last() ) ; :: thesis: verum