let G1 be connected _Graph; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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() ; :: thesis: 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;

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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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() ; :: thesis: 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 :: thesis: for u, v being Vertex of G2 ex W being Walk of G2 st W is_Walk_from u,v

hence
G2 is connected
; :: thesis: verumlet u, v be Vertex of G2; :: thesis: 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;

end;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 :: thesis: ex W being Walk of G2 st W is_Walk_from u,vend;

hence
ex W being Walk of G2 st W is_Walk_from u,v
; :: thesis: verumper cases
( e in the Path of C .edges() or not e in the Path of C .edges() )
;

end;

suppose
e in the Path of C .edges()
; :: thesis: ex W being Walk of G2 st W is_Walk_from u,v

then 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;

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;

end;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 :: thesis: not e in ( the Path of C .cut (1,m)) .edges()

then reconsider P19 = the Path of C .cut (1,m) as Walk of G2 by GLIB_001:172;assume
e in ( the Path of C .cut (1,m)) .edges()
; :: thesis: contradiction

then 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; :: thesis: verum

end;then 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; :: thesis: verum

now :: thesis: not e in ( the Path of C .cut ((m + 2),(len the Path of C))) .edges()

then reconsider P29 = the Path of C .cut ((m + 2),(len the Path of C)) as Walk of G2 by GLIB_001:172;assume
e in ( the Path of C .cut ((m + 2),(len the Path of C))) .edges()
; :: thesis: contradiction

then 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; :: thesis: verum

end;then 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; :: thesis: verum

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;

now :: thesis: ex W being Walk of G2 st W is_Walk_from u,vend;

hence
ex W being Walk of G2 st W is_Walk_from u,v
; :: thesis: verumper cases
( ( a = v1 & b = v2 ) or ( b = v1 & a = v2 ) )
by A15, GLIB_000:def 13;

end;

suppose
( a = v1 & b = v2 )
; :: thesis: ex W being Walk of G2 st W is_Walk_from u,v

then
P19 .append X2 is_Walk_from u,b
by A5, A29, GLIB_001:31;

then (P19 .append X2) .append P29 is_Walk_from u,v by A30, GLIB_001:31;

hence ex W being Walk of G2 st W is_Walk_from u,v ; :: thesis: verum

end;then (P19 .append X2) .append P29 is_Walk_from u,v by A30, GLIB_001:31;

hence ex W being Walk of G2 st W is_Walk_from u,v ; :: thesis: verum

suppose
( b = v1 & a = v2 )
; :: thesis: ex W being Walk of G2 st W is_Walk_from u,v

then
P19 .append (X2 .reverse()) is_Walk_from u,b
by A6, A29, GLIB_001:31;

then (P19 .append (X2 .reverse())) .append P29 is_Walk_from u,v by A30, GLIB_001:31;

hence ex W being Walk of G2 st W is_Walk_from u,v ; :: thesis: verum

end;then (P19 .append (X2 .reverse())) .append P29 is_Walk_from u,v by A30, GLIB_001:31;

hence ex W being Walk of G2 st W is_Walk_from u,v ; :: thesis: verum

suppose
not e in the Path of C .edges()
; :: thesis: ex P being Walk of G2 st P is_Walk_from u,v

then reconsider P = the Path of C as Walk of G2 by GLIB_001:172;

take P = P; :: thesis: P is_Walk_from u,v

thus P is_Walk_from u,v by A8, GLIB_001:19; :: thesis: verum

end;take P = P; :: thesis: P is_Walk_from u,v

thus P is_Walk_from u,v by A8, GLIB_001:19; :: thesis: verum