let G1 be non trivial connected _Graph; :: thesis: for v being Vertex of G1

for G2 being removeVertex of G1,v st v is endvertex holds

G2 is connected

let v be Vertex of G1; :: thesis: for G2 being removeVertex of G1,v st v is endvertex holds

G2 is connected

let G2 be removeVertex of G1,v; :: thesis: ( v is endvertex implies G2 is connected )

set VG = the_Vertices_of G1;

set VG2 = the_Vertices_of G2;

assume A1: v is endvertex ; :: thesis: G2 is connected

then consider ev being object such that

A2: v .edgesInOut() = {ev} and

not ev Joins v,v,G1 by GLIB_000:def 51;

for G2 being removeVertex of G1,v st v is endvertex holds

G2 is connected

let v be Vertex of G1; :: thesis: for G2 being removeVertex of G1,v st v is endvertex holds

G2 is connected

let G2 be removeVertex of G1,v; :: thesis: ( v is endvertex implies G2 is connected )

set VG = the_Vertices_of G1;

set VG2 = the_Vertices_of G2;

assume A1: v is endvertex ; :: thesis: G2 is connected

then consider ev being object such that

A2: v .edgesInOut() = {ev} and

not ev Joins v,v,G1 by GLIB_000:def 51;

now :: thesis: for v19, v29 being Vertex of G2 ex W being Walk of G2 st W is_Walk_from v19,v29

hence
G2 is connected
; :: thesis: verumlet v19, v29 be Vertex of G2; :: thesis: ex W being Walk of G2 st W is_Walk_from v19,v29

reconsider v1 = v19, v2 = v29 as Vertex of G1 by GLIB_000:42;

consider W being Walk of G1 such that

A3: W is_Walk_from v1,v2 by Def1;

set T = the Trail of W;

A4: the Trail of W is_Walk_from v1,v2 by A3, GLIB_001:160;

then A5: the Trail of W . (len the Trail of W) = v2 by GLIB_001:17;

v19 in the_Vertices_of G2 ;

then v19 in (the_Vertices_of G1) \ {v} by GLIB_000:47;

then A6: not v1 in {v} by XBOOLE_0:def 5;

v29 in the_Vertices_of G2 ;

then v29 in (the_Vertices_of G1) \ {v} by GLIB_000:47;

then not v2 in {v} by XBOOLE_0:def 5;

then A7: v2 <> v by TARSKI:def 1;

A8: the Trail of W . 1 = v1 by A4, GLIB_001:17;

A30: v1 <> v by A6, TARSKI:def 1;

then reconsider W9 = the Trail of W as Walk of G2 by A29, GLIB_001:170;

W9 is_Walk_from v19,v29 by A4, GLIB_001:19;

hence ex W being Walk of G2 st W is_Walk_from v19,v29 ; :: thesis: verum

end;reconsider v1 = v19, v2 = v29 as Vertex of G1 by GLIB_000:42;

consider W being Walk of G1 such that

A3: W is_Walk_from v1,v2 by Def1;

set T = the Trail of W;

A4: the Trail of W is_Walk_from v1,v2 by A3, GLIB_001:160;

then A5: the Trail of W . (len the Trail of W) = v2 by GLIB_001:17;

v19 in the_Vertices_of G2 ;

then v19 in (the_Vertices_of G1) \ {v} by GLIB_000:47;

then A6: not v1 in {v} by XBOOLE_0:def 5;

v29 in the_Vertices_of G2 ;

then v29 in (the_Vertices_of G1) \ {v} by GLIB_000:47;

then not v2 in {v} by XBOOLE_0:def 5;

then A7: v2 <> v by TARSKI:def 1;

A8: the Trail of W . 1 = v1 by A4, GLIB_001:17;

now :: thesis: for e being object st e in the Trail of W .edges() holds

e in the_Edges_of G2

then A29:
the Trail of W .edges() c= the_Edges_of G2
;e in the_Edges_of G2

let e be object ; :: thesis: ( e in the Trail of W .edges() implies e in the_Edges_of G2 )

assume A9: e in the Trail of W .edges() ; :: thesis: e in the_Edges_of G2

then consider n being even Element of NAT such that

A10: 1 <= n and

A11: n <= len the Trail of W and

A12: the Trail of W . n = e by GLIB_001:99;

n in dom the Trail of W by A10, A11, FINSEQ_3:25;

then consider n1 being odd Element of NAT such that

A13: n1 = n - 1 and

A14: n - 1 in dom the Trail of W and

A15: n + 1 in dom the Trail of W and

A16: the Trail of W . n Joins the Trail of W . n1, the Trail of W . (n + 1),G1 by GLIB_001:9;

A17: n + 1 <= len the Trail of W by A15, FINSEQ_3:25;

A18: n1 <= len the Trail of W by A13, A14, FINSEQ_3:25;

then e in (the_Edges_of G1) \ (G1 .edgesInOut {v}) by GLIB_000:def 40;

then e in G1 .edgesBetween ((the_Vertices_of G1) \ {v}) by GLIB_000:35;

hence e in the_Edges_of G2 by GLIB_000:47; :: thesis: verum

end;assume A9: e in the Trail of W .edges() ; :: thesis: e in the_Edges_of G2

then consider n being even Element of NAT such that

A10: 1 <= n and

A11: n <= len the Trail of W and

A12: the Trail of W . n = e by GLIB_001:99;

n in dom the Trail of W by A10, A11, FINSEQ_3:25;

then consider n1 being odd Element of NAT such that

A13: n1 = n - 1 and

A14: n - 1 in dom the Trail of W and

A15: n + 1 in dom the Trail of W and

A16: the Trail of W . n Joins the Trail of W . n1, the Trail of W . (n + 1),G1 by GLIB_001:9;

A17: n + 1 <= len the Trail of W by A15, FINSEQ_3:25;

A18: n1 <= len the Trail of W by A13, A14, FINSEQ_3:25;

now :: thesis: not e in v .edgesInOut()

then
e in (the_Edges_of G1) \ (v .edgesInOut())
by A9, XBOOLE_0:def 5;assume A19:
e in v .edgesInOut()
; :: thesis: contradiction

then A20: e = ev by A2, TARSKI:def 1;

end;then A20: e = ev by A2, TARSKI:def 1;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( the Trail of W . n1 = v or the Trail of W . (n + 1) = v )
by A12, A16, A19, GLIB_000:65;

end;

suppose A21:
the Trail of W . n1 = v
; :: thesis: contradiction

reconsider n2 = n1 - 1 as even Element of NAT by ABIAN:12, INT_1:5;

A22: 1 <= n1 by ABIAN:12;

n1 <> 1 by A6, A8, A21, TARSKI:def 1;

then A23: 1 < n1 by A22, XXREAL_0:1;

then 1 + 1 <= n1 by NAT_1:13;

then A24: (1 + 1) - 1 <= n2 by XREAL_1:13;

the Trail of W .vertexAt n1 = v by A18, A21, GLIB_001:def 8;

then the Trail of W . n2 in v .edgesInOut() by A18, A23, GLIB_001:11;

then A25: the Trail of W . n = the Trail of W . n2 by A2, A12, A20, TARSKI:def 1;

n - 1 < n - 0 by XREAL_1:15;

then n1 - 1 < n - 0 by A13, XREAL_1:14;

hence contradiction by A11, A25, A24, GLIB_001:138; :: thesis: verum

end;A22: 1 <= n1 by ABIAN:12;

n1 <> 1 by A6, A8, A21, TARSKI:def 1;

then A23: 1 < n1 by A22, XXREAL_0:1;

then 1 + 1 <= n1 by NAT_1:13;

then A24: (1 + 1) - 1 <= n2 by XREAL_1:13;

the Trail of W .vertexAt n1 = v by A18, A21, GLIB_001:def 8;

then the Trail of W . n2 in v .edgesInOut() by A18, A23, GLIB_001:11;

then A25: the Trail of W . n = the Trail of W . n2 by A2, A12, A20, TARSKI:def 1;

n - 1 < n - 0 by XREAL_1:15;

then n1 - 1 < n - 0 by A13, XREAL_1:14;

hence contradiction by A11, A25, A24, GLIB_001:138; :: thesis: verum

suppose A26:
the Trail of W . (n + 1) = v
; :: thesis: contradiction

then A27:
n + 1 < len the Trail of W
by A7, A5, A17, XXREAL_0:1;

the Trail of W .vertexAt (n + 1) = v by A17, A26, GLIB_001:def 8;

then the Trail of W . ((n + 1) + 1) in v .edgesInOut() by A27, GLIB_001:10;

then A28: the Trail of W . n = the Trail of W . ((n + 1) + 1) by A2, A12, A20, TARSKI:def 1;

( n + 0 < n + (1 + 1) & (n + 1) + 1 <= len the Trail of W ) by A27, NAT_1:13, XREAL_1:8;

hence contradiction by A10, A28, GLIB_001:138; :: thesis: verum

end;the Trail of W .vertexAt (n + 1) = v by A17, A26, GLIB_001:def 8;

then the Trail of W . ((n + 1) + 1) in v .edgesInOut() by A27, GLIB_001:10;

then A28: the Trail of W . n = the Trail of W . ((n + 1) + 1) by A2, A12, A20, TARSKI:def 1;

( n + 0 < n + (1 + 1) & (n + 1) + 1 <= len the Trail of W ) by A27, NAT_1:13, XREAL_1:8;

hence contradiction by A10, A28, GLIB_001:138; :: thesis: verum

then e in (the_Edges_of G1) \ (G1 .edgesInOut {v}) by GLIB_000:def 40;

then e in G1 .edgesBetween ((the_Vertices_of G1) \ {v}) by GLIB_000:35;

hence e in the_Edges_of G2 by GLIB_000:47; :: thesis: verum

A30: v1 <> v by A6, TARSKI:def 1;

now :: thesis: for x being object st x in the Trail of W .vertices() holds

x in the_Vertices_of G2

then
the Trail of W .vertices() c= the_Vertices_of G2
;x in the_Vertices_of G2

let x be object ; :: thesis: ( x in the Trail of W .vertices() implies x in the_Vertices_of G2 )

assume A31: x in the Trail of W .vertices() ; :: thesis: x in the_Vertices_of G2

then x in (the_Vertices_of G1) \ {v} by A31, XBOOLE_0:def 5;

hence x in the_Vertices_of G2 by GLIB_000:47; :: thesis: verum

end;assume A31: x in the Trail of W .vertices() ; :: thesis: x in the_Vertices_of G2

now :: thesis: not x = v

then
not x in {v}
by TARSKI:def 1;assume
x = v
; :: thesis: contradiction

then ( v = the Trail of W .first() or v = the Trail of W .last() ) by A1, A31, GLIB_001:143;

hence contradiction by A30, A7, A4, GLIB_001:def 23; :: thesis: verum

end;then ( v = the Trail of W .first() or v = the Trail of W .last() ) by A1, A31, GLIB_001:143;

hence contradiction by A30, A7, A4, GLIB_001:def 23; :: thesis: verum

then x in (the_Vertices_of G1) \ {v} by A31, XBOOLE_0:def 5;

hence x in the_Vertices_of G2 by GLIB_000:47; :: thesis: verum

then reconsider W9 = the Trail of W as Walk of G2 by A29, GLIB_001:170;

W9 is_Walk_from v19,v29 by A4, GLIB_001:19;

hence ex W being Walk of G2 st W is_Walk_from v19,v29 ; :: thesis: verum