let G1 be non trivial connected _Graph; :: thesis:
let v be Vertex of G1; :: thesis:
let G2 be removeVertex of G1,v; :: thesis:
set VG = the_Vertices_of G1;
set VG2 = the_Vertices_of G2;
assume A1: v is endvertex ; :: thesis:
then consider ev being set such that
A2: v .edgesInOut() = {ev} and
not ev Joins v,v,G1 by GLIB_000:def 53;

now

let v19, v29 be Vertex of G2; :: thesis:
reconsider v1 = v19, v2 = v29 as Vertex of G1 by GLIB_000:45;
consider W being Walk of G1 such that
A3: W is_Walk_from v1,v2 by Def1;
consider T being Trail of W;
A4: T is_Walk_from v1,v2 by A3, GLIB_001:161;
then A5: T . (len T) = v2 by GLIB_001:18;
v19 in the_Vertices_of G2 ;
then v19 in (the_Vertices_of G1) \ {v} by GLIB_000:50;
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:50;
then not v2 in {v} by XBOOLE_0:def 5;
then A7: v2 <> v by TARSKI:def 1;
A8: T . 1 = v1 by A4, GLIB_001:18;

now

let e be set ; :: thesis:
assume A9: e in T .edges() ; :: thesis:
then consider n being even Element of NAT such that
A10: 1 <= n and
A11: n <= len T and
A12: T . n = e by GLIB_001:100;
n in dom T by A10, A11, FINSEQ_3:27;
then consider n1 being odd Element of NAT such that
A13: n1 = n - 1 and
A14: n - 1 in dom T and
A15: n + 1 in dom T and
A16: T . n Joins T . n1,T . (n + 1),G1 by GLIB_001:10;
A17: n + 1 <= len T by A15, FINSEQ_3:27;
A18: n1 <= len T by A13, A14, FINSEQ_3:27;

now

assume A19: e in v .edgesInOut() ; :: thesis:
then A20: e = ev by A2, TARSKI:def 1;

now

per cases by A12, A16, A19, GLIB_000:68;

suppose A21: T . n1 = v ; :: thesis:

reconsider n2 = n1 - 1 as even Element of NAT by HEYTING3:1, INT_1:18;
A22: 1 <= n1 by HEYTING3:1;
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:15;
T .vertexAt n1 = v by A18, A21, GLIB_001:def 8;
then T . n2 in v .edgesInOut() by A18, A23, GLIB_001:12;
then A25: T . n = T . n2 by A2, A12, A20, TARSKI:def 1;
n - 1 < n - 0 by XREAL_1:17;
then n1 - 1 < n - 0 by A13, XREAL_1:16;
hence contradiction by A11, A25, A24, GLIB_001:139; :: thesis:

end;

suppose A26: T . (n + 1) = v ; :: thesis:

then A27: n + 1 < len T by A7, A5, A17, XXREAL_0:1;
T .vertexAt (n + 1) = v by A17, A26, GLIB_001:def 8;
then T . ((n + 1) + 1) in v .edgesInOut() by A27, GLIB_001:11;
then A28: T . n = T . ((n + 1) + 1) by A2, A12, A20, TARSKI:def 1;
( n + 0 < n + (1 + 1) & (n + 1) + 1 <= len T ) by A27, NAT_1:13, XREAL_1:10;
hence contradiction by A10, A28, GLIB_001:139; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

then e in (the_Edges_of G1) \ (v .edgesInOut() ) by A9, XBOOLE_0:def 5;
then e in (the_Edges_of G1) \ (G1 .edgesInOut {v}) by GLIB_000:def 42;
then e in G1 .edgesBetween ((the_Vertices_of G1) \ {v}) by GLIB_000:38;
hence e in the_Edges_of G2 by GLIB_000:50; :: thesis:

end;

then A29: T .edges() c= the_Edges_of G2 by TARSKI:def 3;
A30: v1 <> v by A6, TARSKI:def 1;

now

let x be set ; :: thesis:
assume A31: x in T .vertices() ; :: thesis:

now

assume x = v ; :: thesis:
then ( v = T .first() or v = T .last() ) by A1, A31, GLIB_001:144;
hence contradiction by A30, A7, A4, GLIB_001:def 23; :: thesis:

end;

then not x in {v} by TARSKI:def 1;
then x in (the_Vertices_of G1) \ {v} by A31, XBOOLE_0:def 5;
hence x in the_Vertices_of G2 by GLIB_000:50; :: thesis:

end;

then T .vertices() c= the_Vertices_of G2 by TARSKI:def 3;
then reconsider W9 = T as Walk of G2 by A29, GLIB_001:171;
W9 is_Walk_from v19,v29 by A4, GLIB_001:20;
hence ex W being Walk of G2 st W is_Walk_from v19,v29 ; :: thesis:

end;

hence G2 is connected by Def1; :: thesis: