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;
now :: thesis: for v19, v29 being Vertex of G2 ex W being Walk of G2 st W is_Walk_from v19,v29
let 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 ;
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 () \ {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 () \ {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 ;
now :: thesis: for e being object st e in the Trail of W .edges() holds
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:
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 ;
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 ;
A18: n1 <= len the Trail of W by ;
now :: thesis: not e in v .edgesInOut()
assume A19: e in v .edgesInOut() ; :: thesis: contradiction
then A20: e = ev by ;
now :: thesis: contradiction
per cases ( the Trail of W . n1 = v or the Trail of W . (n + 1) = v ) by ;
suppose A21: the Trail of W . n1 = v ; :: thesis: contradiction
reconsider n2 = n1 - 1 as even Element of NAT by ;
A22: 1 <= n1 by ABIAN:12;
n1 <> 1 by ;
then A23: 1 < n1 by ;
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 ;
then the Trail of W . n2 in v .edgesInOut() by ;
then A25: the Trail of W . n = the Trail of W . n2 by ;
n - 1 < n - 0 by XREAL_1:15;
then n1 - 1 < n - 0 by ;
hence contradiction by A11, A25, A24, GLIB_001:138; :: thesis: verum
end;
suppose A26: the Trail of W . (n + 1) = v ; :: thesis: contradiction
then A27: n + 1 < len the Trail of W by ;
the Trail of W .vertexAt (n + 1) = v by ;
then the Trail of W . ((n + 1) + 1) in v .edgesInOut() by ;
then A28: the Trail of W . n = the Trail of W . ((n + 1) + 1) by ;
( n + 0 < n + (1 + 1) & (n + 1) + 1 <= len the Trail of W ) by ;
hence contradiction by A10, A28, GLIB_001:138; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
then e in () \ () by ;
then e in () \ () by GLIB_000:def 40;
then e in G1 .edgesBetween (() \ {v}) by GLIB_000:35;
hence e in the_Edges_of G2 by GLIB_000:47; :: thesis: verum
end;
then A29: the Trail of W .edges() c= the_Edges_of G2 ;
A30: v1 <> v by ;
now :: thesis: for x being object st x in the Trail of W .vertices() holds
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:
now :: thesis: not x = v
assume x = v ; :: thesis: contradiction
then ( v = the Trail of W .first() or v = the Trail of W .last() ) by ;
hence contradiction by A30, A7, A4, GLIB_001:def 23; :: thesis: verum
end;
then not x in {v} by TARSKI:def 1;
then x in () \ {v} by ;
hence x in the_Vertices_of G2 by GLIB_000:47; :: thesis: verum
end;
then the Trail of W .vertices() c= the_Vertices_of G2 ;
then reconsider W9 = the Trail of W as Walk of G2 by ;
W9 is_Walk_from v19,v29 by ;
hence ex W being Walk of G2 st W is_Walk_from v19,v29 ; :: thesis: verum
end;
hence G2 is connected ; :: thesis: verum