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 )
assume A1:
v is endvertex
; :: thesis: G2 is connected
then consider ev being set such that
A2:
( v .edgesInOut() = {ev} & not ev Joins v,v,G1 )
by GLIB_000:def 53;
set VG = the_Vertices_of G1;
set VG2 = the_Vertices_of G2;
now let v1',
v2' be
Vertex of
G2;
:: thesis: ex W being Walk of G2 st W is_Walk_from v1',v2'reconsider v1 =
v1',
v2 =
v2' 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;
(
v1' in the_Vertices_of G2 &
v2' in the_Vertices_of G2 )
;
then
(
v1' in (the_Vertices_of G1) \ {v} &
v2' in (the_Vertices_of G1) \ {v} )
by GLIB_000:50;
then A4:
( not
v1 in {v} & not
v2 in {v} )
by XBOOLE_0:def 5;
then A5:
(
v1 <> v &
v2 <> v )
by TARSKI:def 1;
consider T being
Trail of
W;
A6:
T is_Walk_from v1,
v2
by A3, GLIB_001:161;
then A8:
T .vertices() c= the_Vertices_of G2
by TARSKI:def 3;
A9:
(
T . 1
= v1 &
T . (len T) = v2 )
by A6, GLIB_001:18;
now let e be
set ;
:: thesis: ( e in T .edges() implies e in the_Edges_of G2 )assume A10:
e in T .edges()
;
:: thesis: e in the_Edges_of G2then consider n being
even Element of
NAT such that A11:
( 1
<= n &
n <= len T &
T . n = e )
by GLIB_001:100;
n in dom T
by A11, FINSEQ_3:27;
then consider n1 being
odd Element of
NAT such that A12:
(
n1 = n - 1 &
n - 1
in dom T &
n + 1
in dom T &
T . n Joins T . n1,
T . (n + 1),
G1 )
by GLIB_001:10;
A13:
(
n1 <= len T &
n + 1
<= len T )
by A12, FINSEQ_3:27;
now assume A14:
e in v .edgesInOut()
;
:: thesis: contradictionthen A15:
e = ev
by A2, TARSKI:def 1;
now per cases
( T . n1 = v or T . (n + 1) = v )
by A11, A12, A14, GLIB_000:68;
suppose A16:
T . n1 = v
;
:: thesis: contradictionthen A17:
T .vertexAt n1 = v
by A13, GLIB_001:def 8;
A18:
n1 <> 1
by A4, A9, A16, TARSKI:def 1;
1
<= n1
by HEYTING3:1;
then A19:
1
< n1
by A18, XXREAL_0:1;
reconsider n2 =
n1 - 1 as
even Element of
NAT by HEYTING3:1, INT_1:18;
T . n2 in v .edgesInOut()
by A13, A17, A19, GLIB_001:12;
then A20:
T . n = T . n2
by A2, A11, A15, TARSKI:def 1;
n - 1
< n - 0
by XREAL_1:17;
then A21:
n1 - 1
< n - 0
by A12, XREAL_1:16;
1
+ 1
<= n1
by A19, NAT_1:13;
then
(1 + 1) - 1
<= n2
by XREAL_1:15;
hence
contradiction
by A11, A20, A21, GLIB_001:139;
:: thesis: verum end; suppose A22:
T . (n + 1) = v
;
:: thesis: contradictionthen A23:
T .vertexAt (n + 1) = v
by A13, GLIB_001:def 8;
A24:
n + 1
< len T
by A5, A9, A13, A22, XXREAL_0:1;
then
T . ((n + 1) + 1) in v .edgesInOut()
by A23, GLIB_001:11;
then A25:
T . n = T . ((n + 1) + 1)
by A2, A11, A15, TARSKI:def 1;
A26:
n + 0 < n + (1 + 1)
by XREAL_1:10;
(n + 1) + 1
<= len T
by A24, NAT_1:13;
hence
contradiction
by A11, A25, A26, GLIB_001:139;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum end; then
e in (the_Edges_of G1) \ (v .edgesInOut() )
by A10, 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: verum end; then
T .edges() c= the_Edges_of G2
by TARSKI:def 3;
then reconsider W' =
T as
Walk of
G2 by A8, GLIB_001:171;
W' is_Walk_from v1',
v2'
by A6, GLIB_001:20;
hence
ex
W being
Walk of
G2 st
W is_Walk_from v1',
v2'
;
:: thesis: verum end;
hence
G2 is connected
by Def1; :: thesis: verum