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 V5() or not P2 is V5() or ( P1 is V5() & P2 is V5() ) ) ;
suppose P1 is V5() ; :: thesis: P1 .append P2 is Path-like
hence P1 .append P2 is Path-like by A1, Th16; :: thesis: verum
end;
suppose P2 is V5() ; :: thesis: P1 .append P2 is Path-like
hence P1 .append P2 is Path-like by GLIB_001:130; :: thesis: verum
end;
suppose ( P1 is V5() & P2 is V5() ) ; :: thesis: P1 .append P2 is Path-like
hence P1 .append P2 is Path-like by A1, A2, Th19; :: thesis: verum
end;
end;