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 = () . e, v2 = () . e as Vertex of G1 by ;
e Joins v1,v2,G1 by ;
then consider X being Walk of G1 such that
A3: X is_Walk_from v1,v2 and
A4: not e in X .edges() by ;
reconsider X2 = X as Walk of G2 by ;
A5: X2 is_Walk_from v1,v2 by ;
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
let 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 ;
then A9: the Path of C . (len the Path of C) = v by GLIB_001:17;
A10: the Path of C . 1 = u by ;
now :: thesis: ex W being Walk of G2 st W is_Walk_from u,v
per 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() ; :: 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 ;
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()
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 ;
then A21: x < m + 1 by NAT_1:13;
x in dom ( the Path of C .cut (1,m)) by ;
then the Path of C . x = e by ;
hence contradiction by A13, A17, A18, A21, GLIB_001:138; :: thesis: verum
end;
then reconsider P19 = the Path of C .cut (1,m) as Walk of G2 by GLIB_001:172;
now :: thesis: 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() ; :: 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 ;
A25: x1 < (len ( the Path of C .cut ((m + 2),(len the Path of C)))) - 0 by ;
then (m + 2) + x1 in dom the Path of C by ;
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 ;
m + 1 < (m + 1) + 1 by NAT_1:13;
then A28: (m + 1) + 0 < (m + 2) + x1 by ;
1 <= m + 1 by NAT_1:12;
hence contradiction by A13, A27, A26, A28, GLIB_001:138; :: thesis: 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 ;
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 ;
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,v
per cases ( ( a = v1 & b = v2 ) or ( b = v1 & a = v2 ) ) by ;
suppose ( a = v1 & b = v2 ) ; :: thesis: ex W being Walk of G2 st W is_Walk_from u,v
end;
suppose ( b = v1 & a = v2 ) ; :: thesis: ex W being Walk of G2 st W is_Walk_from u,v
end;
end;
end;
hence ex W being Walk of G2 st W is_Walk_from u,v ; :: thesis: verum
end;
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 ; :: thesis: verum
end;
end;
end;
hence ex W being Walk of G2 st W is_Walk_from u,v ; :: thesis: verum
end;
hence G2 is connected ; :: thesis: verum