let G2 be _Graph; for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st
for w being Vertex of G3 holds not w in V holds
not G1 is connected
let v be object ; for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st
for w being Vertex of G3 holds not w in V holds
not G1 is connected
let V be set ; for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st
for w being Vertex of G3 holds not w in V holds
not G1 is connected
let G1 be addAdjVertexAll of G2,v,V; ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st
for w being Vertex of G3 holds not w in V implies not G1 is connected )
assume that
A1:
( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 )
and
A2:
ex G3 being Component of G2 st
for w being Vertex of G3 holds not w in V
; not G1 is connected
consider G3 being Component of G2 such that
A3:
for w being Vertex of G3 holds not w in V
by A2;
set v1 = the Vertex of G3;
A4:
the_Vertices_of G3 c= the_Vertices_of G2
;
then A5:
the Vertex of G3 in the_Vertices_of G2
by TARSKI:def 3;
then A6:
the Vertex of G3 <> v
by A1;
A7:
the_Vertices_of G1 = (the_Vertices_of G2) \/ {v}
by A1, Def4;
v in {v}
by TARSKI:def 1;
then A8:
v in the_Vertices_of G1
by A7, XBOOLE_0:def 3;
A9:
the Vertex of G3 in the_Vertices_of G1
by A5, A7, XBOOLE_0:def 3;
for W being Walk of G1 holds not W is_Walk_from the Vertex of G3,v
proof
given W being
Walk of
G1 such that A10:
W is_Walk_from the
Vertex of
G3,
v
;
contradiction
set P = the
Path of
W;
reconsider u1 = the
Vertex of
G3,
u2 =
v as
set by TARSKI:1;
the
Path of
W is_Walk_from u1,
u2
by A10, GLIB_001:160;
then A11:
( the
Path of
W .first() = the
Vertex of
G3 & the
Path of
W .last() = v )
by GLIB_001:def 23;
then
the
Path of
W .first() <> the
Path of
W .last()
by A6;
then
the
Path of
W is
trivial
by GLIB_001:127;
then
3
<= len the
Path of
W
by GLIB_001:125;
then
1
< len the
Path of
W
by XXREAL_0:2;
then reconsider m =
(len the Path of W) - 2 as
odd Element of
NAT by Lm13;
A12:
(
m < (len the Path of W) - 0 &
m <= (len the Path of W) - 0 )
by XREAL_1:15;
set P2 = the
Path of
W .cut (1,
m);
A13:
len ( the Path of W .cut (1,m)) = m
by A12, GLIB_001:45;
not
v in ( the Path of W .cut (1,m)) .vertices()
proof
assume
v in ( the Path of W .cut (1,m)) .vertices()
;
contradiction
then consider k being
odd Element of
NAT such that A14:
(
k <= len ( the Path of W .cut (1,m)) &
( the Path of W .cut (1,m)) . k = v )
by GLIB_001:87;
1
<= k
by ABIAN:12;
then
k in dom ( the Path of W .cut (1,m))
by A14, FINSEQ_3:25;
then
the
Path of
W . k = ( the Path of W .cut (1,m)) . k
by A12, GLIB_001:46;
then A15:
the
Path of
W . k = v
by A14;
A16:
the
Path of
W . (len the Path of W) = v
by A11, GLIB_001:def 7;
k < len the
Path of
W
by A14, A13, A12, XXREAL_0:2;
then
k = 1
by A15, A16, GLIB_001:def 28;
then
the
Path of
W . 1
= v
by A15;
hence
contradiction
by A11, A6, GLIB_001:def 6;
verum
end;
then reconsider P3 = the
Path of
W .cut (1,
m) as
Walk of
G2 by A1, Th64;
A17:
1
<= m
by ABIAN:12;
set v2 =
P3 .last() ;
P3 .last() in the_Vertices_of G3
proof
A18:
1
in dom ( the Path of W .cut (1,m))
by A13, A17, FINSEQ_3:25;
P3 .first() =
( the Path of W .cut (1,m)) . 1
by GLIB_001:def 6
.=
the
Path of
W . 1
by A18, A12, GLIB_001:46
.=
the
Vertex of
G3
by A11, GLIB_001:def 6
;
then A19:
P3 is_Walk_from the
Vertex of
G3,
P3 .last()
by GLIB_001:def 23;
reconsider v3 = the
Vertex of
G3 as
Vertex of
G2 by A4, TARSKI:def 3;
P3 .last() in G2 .reachableFrom v3
by A19, GLIB_002:def 5;
hence
P3 .last() in the_Vertices_of G3
by GLIB_002:33;
verum
end;
then A20:
not
P3 .last() in V
by A3;
P3 .last() =
( the Path of W .cut (1,m)) .last()
by GLIB_001:16
.=
the
Path of
W . m
by A12, A17, Lm16, GLIB_001:37
;
then
the
Path of
W . (m + 1) Joins P3 .last() , the
Path of
W . (m + 2),
G1
by A12, GLIB_001:def 3;
then
the
Path of
W . (m + 1) Joins P3 .last() , the
Path of
W . (len the Path of W),
G1
;
then
the
Path of
W . (m + 1) Joins P3 .last() ,
v,
G1
by GLIB_001:def 7, A11;
hence
contradiction
by A20, A1, Def4;
verum
end;
hence
not G1 is connected
by A8, A9, GLIB_002:def 1; verum