let T be _Tree; :: thesis: for P1, P2 being Path of T st P1 .last() = P2 .first() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} holds
P1 .append P2 is Path-like
let P1, P2 be Path of T; :: thesis: ( P1 .last() = P2 .first() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} implies P1 .append P2 is Path-like )
assume that
A1: P1 .last() = P2 .first() and
A2: (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} ; :: thesis: P1 .append P2 is Path-like

per cases ( not P1 is trivial or not P2 is trivial or ( P1 is trivial & P2 is trivial ) ) ;

suppose P1 is trivial ; :: thesis: P1 .append P2 is Path-like

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

end;

suppose P2 is trivial ; :: thesis: P1 .append P2 is Path-like

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

end;

suppose ( P1 is trivial & P2 is trivial ) ; :: thesis: P1 .append P2 is Path-like

hence P1 .append P2 is Path-like by A1, A2, Th19; :: thesis: verum

end;

end;