let G1 be non _trivial connected _Graph; 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; for G2 being removeVertex of G1,v st v is endvertex holds
G2 is connected
let G2 be removeVertex of G1,v; ( v is endvertex implies G2 is connected )
set VG = the_Vertices_of G1;
set VG2 = the_Vertices_of G2;
assume A1:
v is endvertex
; 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 for v19, v29 being Vertex of G2 ex W being Walk of G2 st W is_Walk_from v19,v29let v19,
v29 be
Vertex of
G2;
ex W being Walk of G2 st W is_Walk_from v19,v29reconsider 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 for e being object st e in the Trail of W .edges() holds
e in the_Edges_of G2let e be
object ;
( e in the Trail of W .edges() implies e in the_Edges_of G2 )assume A9:
e in the
Trail of
W .edges()
;
e in the_Edges_of G2then 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 not e in v .edgesInOut() assume A19:
e in v .edgesInOut()
;
contradictionthen A20:
e = ev
by A2, TARSKI:def 1;
now contradictionper cases
( the Trail of W . n1 = v or the Trail of W . (n + 1) = v )
by A12, A16, A19, GLIB_000:65;
suppose A21:
the
Trail of
W . n1 = v
;
contradictionreconsider 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;
verum end; suppose A26:
the
Trail of
W . (n + 1) = v
;
contradictionthen 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;
verum end; hence
contradiction
;
verum 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 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;
verum end; then A29:
the
Trail of
W .edges() c= the_Edges_of G2
;
A30:
v1 <> v
by A6, TARSKI:def 1;
then
the
Trail of
W .vertices() c= the_Vertices_of G2
;
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
;
verum end;
hence
G2 is connected
; verum