let G be _Graph; :: thesis: for P1, P2 being Path of G st P1 .last() = P2 .first() & not P1 is closed & not P2 is closed & (P1 .vertices() ) /\ (P2 .vertices() ) = {(P1 .last() )} holds
( not P1 .append P2 is closed & P1 .append P2 is Path-like )
let P1, P2 be Path of G; :: thesis: ( P1 .last() = P2 .first() & not P1 is closed & not P2 is closed & (P1 .vertices() ) /\ (P2 .vertices() ) = {(P1 .last() )} implies ( not P1 .append P2 is closed & P1 .append P2 is Path-like ) )
assume that
A1: P1 .last() = P2 .first() and
A2: not P1 is closed and
A3: not P2 is closed and
A4: (P1 .vertices() ) /\ (P2 .vertices() ) = {(P1 .last() )} ; :: thesis: ( not P1 .append P2 is closed & P1 .append P2 is Path-like )
set P = P1 .append P2;
thus not P1 .append P2 is closed :: thesis: P1 .append P2 is Path-like

proof

assume A5: (P1 .append P2) .first() = (P1 .append P2) .last() ; :: according to GLIB_001:def 24 :: thesis: contradiction
( (P1 .append P2) .first() = P1 .first() & (P1 .append P2) .last() = P2 .last() ) by A1, GLIB_001:31;
then ( P1 .first() in P1 .vertices() & P1 .first() in P2 .vertices() ) by A5, GLIB_001:89;
then P1 .first() in {(P1 .last() )} by A4, XBOOLE_0:def 4;
then P1 .first() = P1 .last() by TARSKI:def 1;
hence contradiction by A2, GLIB_001:def 24; :: thesis: verum

end;

A6: now

A7: P1 .first() in P1 .vertices() by GLIB_001:89;
assume P1 .first() in P2 .vertices() ; :: thesis: contradiction
then P1 .first() in {(P1 .last() )} by A4, A7, XBOOLE_0:def 4;
then P1 .first() = P1 .last() by TARSKI:def 1;
hence contradiction by A2, GLIB_001:def 24; :: thesis: verum

end;

A8: P1 .edges() misses P2 .edges()

proof

assume (P1 .edges() ) /\ (P2 .edges() ) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being set such that
A9: x in (P1 .edges() ) /\ (P2 .edges() ) by XBOOLE_0:def 1;
x in P2 .edges() by A9, XBOOLE_0:def 4;
then consider u1, u2 being Vertex of G, m being odd Element of NAT such that
A10: m + 2 <= len P2 and
A11: u1 = P2 . m and
x = P2 . (m + 1) and
A12: u2 = P2 . (m + 2) and
A13: x Joins u1,u2,G by GLIB_001:104;
x in P1 .edges() by A9, XBOOLE_0:def 4;
then consider v1, v2 being Vertex of G, n being odd Element of NAT such that
A14: n + 2 <= len P1 and
A15: v1 = P1 . n and
x = P1 . (n + 1) and
A16: v2 = P1 . (n + 2) and
A17: x Joins v1,v2,G by GLIB_001:104;
A18: n + 0 < n + 2 by XREAL_1:10;

per cases ( v1 <> v2 or v1 = v2 ) ;

suppose A19: v1 <> v2 ; :: thesis: contradiction

n <= len P1 by A14, A18, XXREAL_0:2;
then A20: v1 in P1 .vertices() by A15, GLIB_001:88;
v2 in P1 .vertices() by A14, A16, GLIB_001:88;
then A21: {v1,v2} c= P1 .vertices() by A20, ZFMISC_1:38;
m + 0 < m + 2 by XREAL_1:10;
then m <= len P2 by A10, XXREAL_0:2;
then A22: u1 in P2 .vertices() by A11, GLIB_001:88;
u2 in P2 .vertices() by A10, A12, GLIB_001:88;
then A23: {u1,u2} c= P2 .vertices() by A22, ZFMISC_1:38;
A24: ( ( v1 = u1 & v2 = u2 ) or ( v1 = u2 & v2 = u1 ) ) by A17, A13, GLIB_000:18;
then v1 = P1 .last() by A4, A21, A23, XBOOLE_1:19, ZFMISC_1:26;
hence contradiction by A4, A19, A24, A21, A23, XBOOLE_1:19, ZFMISC_1:26; :: thesis: verum

end;

suppose A25: v1 = v2 ; :: thesis: contradiction

then P1 .first() = v1 by A14, A15, A16, A18, GLIB_001:def 28
.= P1 .last() by A14, A15, A16, A18, A25, GLIB_001:def 28 ;
hence contradiction by A2, GLIB_001:def 24; :: thesis: verum

end;

end;

end;

(P1 .vertices() ) /\ (P2 .vertices() ) c= {(P1 .first() ),(P1 .last() )} by A4, ZFMISC_1:12;
hence P1 .append P2 is Path-like by A1, A2, A3, A8, A6, Th18; :: thesis: verum