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