let T be _Tree; :: thesis:
let P1, P2 be Path of T; :: thesis:
assume that
A1: P1 .last() = P2 .first() and
A2: (P1 .vertices() ) /\ (P2 .vertices() ) = {(P1 .last() )} ; :: thesis:

per cases ;

suppose P1 is trivial ; :: thesis:

hence P1 .append P2 is Path-like by A1, Th15a; :: thesis:

end;

suppose P2 is trivial ; :: thesis:

hence P1 .append P2 is Path-like by GLIB_001:131; :: thesis:

end;

suppose ( not P1 is trivial & not P2 is trivial ) ; :: thesis:

then ( not P1 is closed & not P2 is closed ) ;
hence P1 .append P2 is Path-like by A1, A2, Th18; :: thesis:

end;