let G be _Graph; :: thesis: for P1, P2 being Path of G st P1 .last() = P2 .first() & P2 .last() = P1 .first() & P1 is open & P2 is open & 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() & P1 is open & P2 is open & 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: P1 is open and
A4: ( P2 is open & P1 .edges() misses P2 .edges() & (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:30;
hence P1 .append P2 is closed by A2; :: 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, Th18; :: thesis: not P1 .append P2 is trivial
P1 .first() <> P1 .last() by A3;
then P1 is V5() by GLIB_001:127;
then A5: len P1 >= 3 by GLIB_001:125;
len (P1 .append P2) >= len P1 by A1, GLIB_001:29;
then len (P1 .append P2) >= 3 by A5, XXREAL_0:2;
hence not P1 .append P2 is trivial by GLIB_001:125; :: thesis: verum