let G be _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 )
let P1, P2 be Path of G; ( P1 .last() = P2 .first() & P1 is open & P2 is open & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} implies ( P1 .append P2 is open & P1 .append P2 is Path-like ) )
assume that
A1:
P1 .last() = P2 .first()
and
A2:
P1 is open
and
A3:
P2 is open
and
A4:
(P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())}
; ( P1 .append P2 is open & P1 .append P2 is Path-like )
set P = P1 .append P2;
thus
P1 .append P2 is open
P1 .append P2 is Path-like
A8:
P1 .edges() misses P2 .edges()
proof
assume
(P1 .edges()) /\ (P2 .edges()) <> {}
;
XBOOLE_0:def 7 contradiction
then consider x being
object 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:103;
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:103;
A18:
n + 0 < n + 2
by XREAL_1:8;
per cases
( v1 <> v2 or v1 = v2 )
;
suppose A19:
v1 <> v2
;
contradiction
n <= len P1
by A14, A18, XXREAL_0:2;
then A20:
v1 in P1 .vertices()
by A15, GLIB_001:87;
v2 in P1 .vertices()
by A14, A16, GLIB_001:87;
then A21:
{v1,v2} c= P1 .vertices()
by A20, ZFMISC_1:32;
m + 0 < m + 2
by XREAL_1:8;
then
m <= len P2
by A10, XXREAL_0:2;
then A22:
u1 in P2 .vertices()
by A11, GLIB_001:87;
u2 in P2 .vertices()
by A10, A12, GLIB_001:87;
then A23:
{u1,u2} c= P2 .vertices()
by A22, ZFMISC_1:32;
A24:
( (
v1 = u1 &
v2 = u2 ) or (
v1 = u2 &
v2 = u1 ) )
by A17, A13, GLIB_000:15;
then
v1 = P1 .last()
by A4, A21, A23, XBOOLE_1:19, ZFMISC_1:20;
hence
contradiction
by A4, A19, A24, A21, A23, XBOOLE_1:19, ZFMISC_1:20;
verum end; suppose A25:
v1 = v2
;
contradictionend;
end;
(P1 .vertices()) /\ (P2 .vertices()) c= {(P1 .first()),(P1 .last())}
by A4, ZFMISC_1:7;
hence
P1 .append P2 is Path-like
by A1, A2, A3, A8, A6, Th18; verum