let G be _Graph; for P being Path of G st P is open & len P > 3 holds
for e being object st e Joins P .last() ,P .first() ,G holds
P .addEdge e is Cycle-like
let W be Path of G; ( W is open & len W > 3 implies for e being object st e Joins W .last() ,W .first() ,G holds
W .addEdge e is Cycle-like )
assume that
A1:
W is open
and
A2:
len W > 3
; for e being object st e Joins W .last() ,W .first() ,G holds
W .addEdge e is Cycle-like
let e be object ; ( e Joins W .last() ,W .first() ,G implies W .addEdge e is Cycle-like )
assume A3:
e Joins W .last() ,W .first() ,G
; W .addEdge e is Cycle-like
set P = W .addEdge e;
A12:
(W .addEdge e) .last() = W .first()
by A3, GLIB_001:63;
A13:
len (W .addEdge e) = (len W) + (2 * 1)
by A3, GLIB_001:64;
A14:
now for m, n being odd Element of NAT st m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n holds
( m = 1 & n = len (W .addEdge e) )let m,
n be
odd Element of
NAT ;
( m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n implies ( m = 1 & n = len (W .addEdge e) ) )assume that A15:
m < n
and A16:
n <= len (W .addEdge e)
;
( (W .addEdge e) . m = (W .addEdge e) . n implies ( m = 1 & n = len (W .addEdge e) ) )
m < (len W) + (2 * 1)
by A13, A15, A16, XXREAL_0:2;
then A17:
m <= ((len W) + 2) - 2
by Th3;
assume A18:
(W .addEdge e) . m = (W .addEdge e) . n
;
( m = 1 & n = len (W .addEdge e) )
1
<= m
by Th2;
then A19:
m in dom W
by A17, FINSEQ_3:25;
then A20:
W . m = (W .addEdge e) . m
by A3, GLIB_001:65;
then A24:
(W .addEdge e) . n = W . 1
by A12, A16, XXREAL_0:1;
hence
(
m = 1 &
n = len (W .addEdge e) )
by A16, A21, XXREAL_0:1;
verum end;
e in (W .last()) .edgesInOut()
by A3, GLIB_000:62;
then
W .addEdge e is Trail-like
by A4, GLIB_001:142;
then A26:
W .addEdge e is Path-like
by A14;
(W .addEdge e) .first() = W .first()
by A3, GLIB_001:63;
then A27:
W .addEdge e is closed
by A12;
W .addEdge e is V5()
by A3, GLIB_001:132;
hence
W .addEdge e is Cycle-like
by A27, A26; verum