let G be _Graph; :: thesis: for P1, P2 being Path of G st P1 .last() = P2 .first() & P2 .last() = P1 .first() & not P1 is closed & not P2 is closed & P1 .edges() misses P2 .edges() & (P1 .vertices() ) /\ (P2 .vertices() ) = {(P1 .last() ),(P1 .first() )} holds
P1 .append P2 is Cycle-like
let P1, P2 be Path of G; :: thesis: ( P1 .last() = P2 .first() & P2 .last() = P1 .first() & not P1 is closed & not P2 is closed & P1 .edges() misses P2 .edges() & (P1 .vertices() ) /\ (P2 .vertices() ) = {(P1 .last() ),(P1 .first() )} implies P1 .append P2 is Cycle-like )
assume that
A1: P1 .last() = P2 .first() and
A2: P2 .last() = P1 .first() and
A3: not P1 is closed and
A4: not P2 is closed and
A5: P1 .edges() misses P2 .edges() and
A6: (P1 .vertices() ) /\ (P2 .vertices() ) = {(P1 .last() ),(P1 .first() )} ; :: thesis: P1 .append P2 is Cycle-like
set P = P1 .append P2;
( (P1 .append P2) .first() = P1 .first() & (P1 .append P2) .last() = P2 .last() ) by A1, GLIB_001:31;
hence P1 .append P2 is closed by A2, GLIB_001:def 24; :: according to GLIB_001:def 31 :: thesis: ( P1 .append P2 is Path-like & not P1 .append P2 is trivial )
thus P1 .append P2 is Path-like by A1, A2, A3, A4, A5, A6, Th17; :: thesis: not P1 .append P2 is trivial
P1 .first() <> P1 .last() by A3, GLIB_001:def 24;
then not P1 is trivial by GLIB_001:128;
then A7: len P1 >= 3 by GLIB_001:126;
len (P1 .append P2) >= len P1 by A1, GLIB_001:30;
then len (P1 .append P2) >= 3 by A7, XXREAL_0:2;
hence not P1 .append P2 is trivial by GLIB_001:126; :: thesis: verum