for G being _Graph
for P1, P2 being Path of G st P1 .last() = P2 .first() & P1 is open & P2 is open & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} holds
( P1 .append P2 is open & P1 .append P2 is Path-like )