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

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