consider W being Walk of T such that
A1: W is_Walk_from a,b by GLIB_002:def 1;
set P = the Path-like Subwalk of W;
take the Path-like Subwalk of W ; :: thesis: the Path-like Subwalk of W is_Walk_from a,b
the Path-like Subwalk of W is_Walk_from W .first() ,W .last() by GLIB_001:def 32;
then the Path-like Subwalk of W is_Walk_from a,W .last() by A1;
hence the Path-like Subwalk of W is_Walk_from a,b by A1; :: thesis: verum