theorem Th38: :: HELLY:38

for T being _Tree
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