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

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