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:5;
e Joins v1,v2,G1
by A2, GLIB_000:def 13;
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:157;
reconsider X2 = X as Walk of G2 by A4, GLIB_001:172;
A5:
X2 is_Walk_from v1,v2
by A3, GLIB_001:19;
then A6:
X2 .reverse() is_Walk_from v2,v1
by GLIB_001:23;
now for u, v being Vertex of G2 ex W being Walk of G2 st W is_Walk_from u,vlet 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 ;
consider C being
Walk of
G1 such that A7:
C is_Walk_from u9,
v9
by Def1;
set P = the
Path of
C;
A8:
the
Path of
C is_Walk_from u9,
v9
by A7, GLIB_001:160;
then A9:
the
Path of
C . (len the Path of C) = v
by GLIB_001:17;
A10:
the
Path of
C . 1
= u
by A8, GLIB_001:17;
now ex W being Walk of G2 st W is_Walk_from u,vper cases
( e in the Path of C .edges() or not e in the Path of C .edges() )
;
suppose
e in the
Path of
C .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 the
Path of
C
and A12:
a = the
Path of
C . m
and A13:
e = the
Path of
C . (m + 1)
and A14:
b = the
Path of
C . (m + 2)
and A15:
e Joins a,
b,
G1
by GLIB_001:103;
set P1 = the
Path of
C .cut (1,
m);
set P2 = the
Path of
C .cut (
(m + 2),
(len the Path of C));
A16:
(m + 2) - 2
< (len the Path of C) - 0
by A11, XREAL_1:15;
then A17:
m + 1
<= len the
Path of
C
by NAT_1:13;
now not e in ( the Path of C .cut (1,m)) .edges() assume
e in ( the Path of C .cut (1,m)) .edges()
;
contradictionthen consider x being
even Element of
NAT such that A18:
1
<= x
and A19:
x <= len ( the Path of C .cut (1,m))
and A20:
( the Path of C .cut (1,m)) . x = e
by GLIB_001:99;
x <= m
by A16, A19, GLIB_001:45;
then A21:
x < m + 1
by NAT_1:13;
x in dom ( the Path of C .cut (1,m))
by A18, A19, FINSEQ_3:25;
then
the
Path of
C . x = e
by A16, A20, GLIB_001:46;
hence
contradiction
by A13, A17, A18, A21, GLIB_001:138;
verum end; then reconsider P19 = the
Path of
C .cut (1,
m) as
Walk of
G2 by GLIB_001:172;
now not e in ( the Path of C .cut ((m + 2),(len the Path of C))) .edges() assume
e in ( the Path of C .cut ((m + 2),(len the Path of C))) .edges()
;
contradictionthen consider x being
even Element of
NAT such that A22:
1
<= x
and A23:
x <= len ( the Path of C .cut ((m + 2),(len the Path of C)))
and A24:
( the Path of C .cut ((m + 2),(len the Path of C))) . x = e
by GLIB_001:99;
reconsider x1 =
x - 1 as
odd Element of
NAT by A22, INT_1:5;
A25:
x1 < (len ( the Path of C .cut ((m + 2),(len the Path of C)))) - 0
by A23, XREAL_1:15;
then
(m + 2) + x1 in dom the
Path of
C
by A11, GLIB_001:36;
then A26:
(m + 2) + x1 <= len the
Path of
C
by FINSEQ_3:25;
x1 + 1
= x
;
then A27:
e = the
Path of
C . ((m + 2) + x1)
by A11, A24, A25, GLIB_001:36;
m + 1
< (m + 1) + 1
by NAT_1:13;
then A28:
(m + 1) + 0 < (m + 2) + x1
by NAT_1:2, XREAL_1:8;
1
<= m + 1
by NAT_1:12;
hence
contradiction
by A13, A27, A26, A28, GLIB_001:138;
verum end; then reconsider P29 = the
Path of
C .cut (
(m + 2),
(len the Path of C)) as
Walk of
G2 by GLIB_001:172;
reconsider a =
a,
b =
b as
Vertex of
G2 by GLIB_000:51;
1
<= m
by ABIAN:12;
then
the
Path of
C .cut (1,
m)
is_Walk_from u,
a
by A10, A12, A16, GLIB_001:37, JORDAN12:2;
then A29:
P19 is_Walk_from u,
a
by GLIB_001:19;
the
Path of
C .cut (
(m + 2),
(len the Path of C))
is_Walk_from b,
v
by A9, A11, A14, GLIB_001:37;
then A30:
P29 is_Walk_from b,
v
by GLIB_001:19;
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
; verum