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;
A5:
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 A6:
x in (P1 .edges() ) /\ (P2 .edges() )
by XBOOLE_0:def 1;
A7:
x in P1 .edges()
by A6, XBOOLE_0:def 4;
A8:
x in P2 .edges()
by A6, XBOOLE_0:def 4;
consider v1,
v2 being
Vertex of
G,
n being
odd Element of
NAT such that A9:
n + 2
<= len P1
and A10:
v1 = P1 . n
and
x = P1 . (n + 1)
and A11:
v2 = P1 . (n + 2)
and A12:
x Joins v1,
v2,
G
by A7, GLIB_001:104;
consider u1,
u2 being
Vertex of
G,
m being
odd Element of
NAT such that A13:
m + 2
<= len P2
and A14:
u1 = P2 . m
and
x = P2 . (m + 1)
and A15:
u2 = P2 . (m + 2)
and A16:
x Joins u1,
u2,
G
by A8, GLIB_001:104;
A17:
n + 0 < n + 2
by XREAL_1:10;
per cases
( v1 <> v2 or v1 = v2 )
;
suppose A18:
v1 <> v2
;
:: thesis: contradiction
n <= len P1
by A9, A17, XXREAL_0:2;
then A19:
v1 in P1 .vertices()
by A10, GLIB_001:88;
A20:
v2 in P1 .vertices()
by A9, A11, GLIB_001:88;
m + 0 < m + 2
by XREAL_1:10;
then
m <= len P2
by A13, XXREAL_0:2;
then A21:
u1 in P2 .vertices()
by A14, GLIB_001:88;
A22:
u2 in P2 .vertices()
by A13, A15, GLIB_001:88;
A23:
( (
v1 = u1 &
v2 = u2 ) or (
v1 = u2 &
v2 = u1 ) )
by A12, A16, GLIB_000:18;
A24:
{v1,v2} c= P1 .vertices()
by A19, A20, ZFMISC_1:38;
{u1,u2} c= P2 .vertices()
by A21, A22, ZFMISC_1:38;
then
(
v1 = P1 .last() &
v2 = P1 .last() )
by A4, A23, A24, XBOOLE_1:19, ZFMISC_1:26;
hence
contradiction
by A18;
:: thesis: verum end; suppose A25:
v1 = v2
;
:: thesis: contradictionthen P1 .first() =
v1
by A9, A10, A11, A17, GLIB_001:def 28
.=
P1 .last()
by A9, A10, A11, A17, A25, GLIB_001:def 28
;
hence
contradiction
by A2, GLIB_001:def 24;
:: thesis: verum end;
end;
thus
not P1 .append P2 is closed
:: thesis: P1 .append P2 is Path-like
(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, A5, A27, Th17; :: thesis: verum