let G1 be connected _Graph; for W being Walk of G1
for e being set
for G2 being removeEdge of G1,e st W is Cycle-like & e in W .edges() holds
G2 is connected
let W be Walk of G1; for e being set
for G2 being removeEdge of G1,e st W is Cycle-like & e in W .edges() holds
G2 is connected
let e be set ; for G2 being removeEdge of G1,e st W is Cycle-like & e in W .edges() holds
G2 is connected
let G2 be removeEdge of G1,e; ( W is Cycle-like & e in W .edges() implies G2 is connected )
assume that
A1:
W is Cycle-like
and
A2:
e in W .edges()
; G2 is connected
reconsider v1 = (the_Source_of G1) . e, v2 = (the_Target_of G1) . e as Vertex of G1 by A2, FUNCT_2:7;
e Joins v1,v2,G1
by A2, GLIB_000:def 15;
then consider X being Walk of G1 such that
A3:
X is_Walk_from v1,v2
and
A4:
not e in X .edges()
by A1, A2, GLIB_001:158;
reconsider X2 = X as Walk of G2 by A4, GLIB_001:173;
A5:
X2 is_Walk_from v1,v2
by A3, GLIB_001:20;
then A6:
X2 .reverse() is_Walk_from v2,v1
by GLIB_001:24;
now let u,
v be
Vertex of
G2;
ex W being Walk of G2 st W is_Walk_from u,v
the_Vertices_of G2 c= the_Vertices_of G1
;
then reconsider u9 =
u,
v9 =
v as
Vertex of
G1 by TARSKI:def 3;
consider C being
Walk of
G1 such that A7:
C is_Walk_from u9,
v9
by Def1;
consider P being
Path of
C;
A8:
P is_Walk_from u9,
v9
by A7, GLIB_001:161;
then A9:
P . (len P) = v
by GLIB_001:18;
A10:
P . 1
= u
by A8, GLIB_001:18;
now per cases
( e in P .edges() or not e in P .edges() )
;
suppose
e in P .edges()
;
ex W being Walk of G2 st W is_Walk_from u,vthen consider a,
b being
Vertex of
G1,
m being
odd Element of
NAT such that A11:
m + 2
<= len P
and A12:
a = P . m
and A13:
e = P . (m + 1)
and A14:
b = P . (m + 2)
and A15:
e Joins a,
b,
G1
by GLIB_001:104;
set P1 =
P .cut (1,
m);
set P2 =
P .cut (
(m + 2),
(len P));
A16:
(m + 2) - 2
< (len P) - 0
by A11, XREAL_1:17;
then A17:
m + 1
<= len P
by NAT_1:13;
now assume
e in (P .cut (1,m)) .edges()
;
contradictionthen consider x being
even Element of
NAT such that A18:
1
<= x
and A19:
x <= len (P .cut (1,m))
and A20:
(P .cut (1,m)) . x = e
by GLIB_001:100;
x <= m
by A16, A19, GLIB_001:46;
then A21:
x < m + 1
by NAT_1:13;
x in dom (P .cut (1,m))
by A18, A19, FINSEQ_3:27;
then
P . x = e
by A16, A20, GLIB_001:47;
hence
contradiction
by A13, A17, A18, A21, GLIB_001:139;
verum end; then reconsider P19 =
P .cut (1,
m) as
Walk of
G2 by GLIB_001:173;
now assume
e in (P .cut ((m + 2),(len P))) .edges()
;
contradictionthen consider x being
even Element of
NAT such that A22:
1
<= x
and A23:
x <= len (P .cut ((m + 2),(len P)))
and A24:
(P .cut ((m + 2),(len P))) . x = e
by GLIB_001:100;
reconsider x1 =
x - 1 as
odd Element of
NAT by A22, INT_1:18;
A25:
x1 < (len (P .cut ((m + 2),(len P)))) - 0
by A23, XREAL_1:17;
then
(m + 2) + x1 in dom P
by A11, GLIB_001:37;
then A26:
(m + 2) + x1 <= len P
by FINSEQ_3:27;
x1 + 1
= x
;
then A27:
e = P . ((m + 2) + x1)
by A11, A24, A25, GLIB_001:37;
m + 1
< (m + 1) + 1
by NAT_1:13;
then A28:
(m + 1) + 0 < (m + 2) + x1
by NAT_1:2, XREAL_1:10;
1
<= m + 1
by NAT_1:12;
hence
contradiction
by A13, A27, A26, A28, GLIB_001:139;
verum end; then reconsider P29 =
P .cut (
(m + 2),
(len P)) as
Walk of
G2 by GLIB_001:173;
reconsider a =
a,
b =
b as
Vertex of
G2 by GLIB_000:54;
1
<= m
by ABIAN:12;
then
P .cut (1,
m)
is_Walk_from u,
a
by A10, A12, A16, GLIB_001:38, JORDAN12:3;
then A29:
P19 is_Walk_from u,
a
by GLIB_001:20;
P .cut (
(m + 2),
(len P))
is_Walk_from b,
v
by A9, A11, A14, GLIB_001:38;
then A30:
P29 is_Walk_from b,
v
by GLIB_001:20;
hence
ex
W being
Walk of
G2 st
W is_Walk_from u,
v
;
verum end; hence
ex
W being
Walk of
G2 st
W is_Walk_from u,
v
;
verum end;
hence
G2 is connected
by Def1; verum