let G be _finite non _trivial connected _Graph; ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )
defpred S1[ Nat] means for G being _finite non _trivial connected _Graph st G .order() = $1 holds
ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex );
now for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]let k be
Nat;
( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )assume A1:
for
n being
Nat st
n < k holds
S1[
n]
;
S1[k]now for G being _finite non _trivial connected _Graph st G .order() = k holds
ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )let G be
_finite non
_trivial connected _Graph;
( G .order() = k implies ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex ) )assume A2:
G .order() = k
;
ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )A3:
G .numComponents() = 1
by Lm18;
now ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )per cases
( for v being Vertex of G holds not v is cut-vertex or ex cv being Vertex of G st cv is cut-vertex )
;
suppose
ex
cv being
Vertex of
G st
cv is
cut-vertex
;
ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )then consider cv being
Vertex of
G such that A6:
cv is
cut-vertex
;
set G2 = the
removeVertex of
G,
cv;
1
< the
removeVertex of
G,
cv .numComponents()
by A3, A6;
then
1
+ 1
<= the
removeVertex of
G,
cv .numComponents()
by NAT_1:13;
then
card 2
<= card ( the removeVertex of G,cv .componentSet())
;
then
Segm (card 2) c= Segm (card ( the removeVertex of G,cv .componentSet()))
by NAT_1:39;
then
2
c= card ( the removeVertex of G,cv .componentSet())
;
then consider C1,
C2 being
object such that A7:
(
C1 in the
removeVertex of
G,
cv .componentSet() &
C2 in the
removeVertex of
G,
cv .componentSet() )
and A8:
C1 <> C2
by PENCIL_1:2;
reconsider C1 =
C1,
C2 =
C2 as
Element of the
removeVertex of
G,
cv .componentSet() by A7;
set CC1 = the
inducedSubgraph of the
removeVertex of
G,
cv,
C1;
set CC2 = the
inducedSubgraph of the
removeVertex of
G,
cv,
C2;
A9:
the_Vertices_of the
removeVertex of
G,
cv = (the_Vertices_of G) \ {cv}
by GLIB_000:47;
G .edgesBetween ((the_Vertices_of G) \ {cv}) = (the_Edges_of G) \ (G .edgesInOut {cv})
by GLIB_000:35;
then
G .edgesBetween ((the_Vertices_of G) \ {cv}) = (the_Edges_of G) \ (cv .edgesInOut())
by GLIB_000:def 40;
then A10:
the_Edges_of the
removeVertex of
G,
cv = (the_Edges_of G) \ (cv .edgesInOut())
by GLIB_000:47;
A11:
( the removeVertex of G,cv .order()) + 1
= k
by A2, GLIB_000:48;
A12:
now for C being Component of the removeVertex of G,cv ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )let C be
Component of the
removeVertex of
G,
cv;
ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )now ex a being Vertex of C ex e being set st e Joins cv,a,Gset x = the
Vertex of
C;
assume A13:
for
a being
Vertex of
C for
e being
set holds not
e Joins cv,
a,
G
;
contradiction
the_Vertices_of C c= the_Vertices_of the
removeVertex of
G,
cv
;
then reconsider x9 = the
Vertex of
C as
Vertex of the
removeVertex of
G,
cv ;
the_Vertices_of the
removeVertex of
G,
cv c= the_Vertices_of G
;
then reconsider x99 =
x9 as
Vertex of
G ;
consider W being
Walk of
G such that A14:
W is_Walk_from cv,
x99
by Def1;
set P = the
Path of
W;
A15:
the
Path of
W is_Walk_from cv,
x99
by A14, GLIB_001:160;
then A16:
the
Path of
W .first() = cv
by GLIB_001:def 23;
set P2 = the
Path of
W .cut (
((2 * 1) + 1),
(len the Path of W));
A17:
1
<= len the
Path of
W
by ABIAN:12;
A18:
the
Path of
W .last() = the
Vertex of
C
by A15, GLIB_001:def 23;
then A19:
the
Path of
W . (len the Path of W) = the
Vertex of
C
by GLIB_001:def 7;
not
x9 in {cv}
by A9, XBOOLE_0:def 5;
then A20:
the
Vertex of
C <> cv
by TARSKI:def 1;
then A21:
the
Path of
W is
trivial
by A16, A18, GLIB_001:127;
then A22:
(2 * 1) + 1
<= len the
Path of
W
by GLIB_001:125;
then
the
Path of
W .cut (
((2 * 1) + 1),
(len the Path of W))
is_Walk_from the
Path of
W . 3, the
Path of
W . (len the Path of W)
by GLIB_001:37;
then A23:
the
Path of
W .cut (
((2 * 1) + 1),
(len the Path of W))
is_Walk_from the
Path of
W . 3, the
Vertex of
C
by A18, GLIB_001:def 7;
A24:
the
Path of
W . ((2 * 0) + 1) = cv
by A16, GLIB_001:def 6;
now not cv in ( the Path of W .cut (((2 * 1) + 1),(len the Path of W))) .vertices() assume
cv in ( the Path of W .cut (((2 * 1) + 1),(len the Path of W))) .vertices()
;
contradictionthen consider n being
odd Element of
NAT such that A25:
n <= len ( the Path of W .cut (((2 * 1) + 1),(len the Path of W)))
and A26:
( the Path of W .cut (((2 * 1) + 1),(len the Path of W))) . n = cv
by GLIB_001:87;
A27:
1
<= n
by ABIAN:12;
then A28:
1
+ 0 < n + 2
by XREAL_1:8;
A29:
n in dom ( the Path of W .cut (((2 * 1) + 1),(len the Path of W)))
by A25, A27, FINSEQ_3:25;
then
(3 + n) - 1
in dom the
Path of
W
by A22, GLIB_001:47;
then A30:
2
+ n <= len the
Path of
W
by FINSEQ_3:25;
the
Path of
W . ((3 + n) - 1) = cv
by A22, A26, A29, GLIB_001:47;
hence
contradiction
by A20, A24, A19, A30, A28, GLIB_001:def 28;
verum end; then reconsider P2 = the
Path of
W .cut (
((2 * 1) + 1),
(len the Path of W)) as
Walk of the
removeVertex of
G,
cv by GLIB_001:171;
P2 is_Walk_from the
Path of
W . 3, the
Vertex of
C
by A23, GLIB_001:19;
then
P2 .reverse() is_Walk_from the
Vertex of
C, the
Path of
W . 3
by GLIB_001:23;
then A31:
the
Path of
W . 3
in the
removeVertex of
G,
cv .reachableFrom x9
by Def5;
len the
Path of
W <> 1
by A21, GLIB_001:125;
then
(2 * 0) + 1
< len the
Path of
W
by A17, XXREAL_0:1;
then
the
Path of
W . (1 + 1) Joins the
Path of
W . 1, the
Path of
W . (1 + 2),
G
by GLIB_001:def 3;
then A32:
the
Path of
W . 2
Joins cv, the
Path of
W . 3,
G
by A16, GLIB_001:def 6;
the_Vertices_of C = the
removeVertex of
G,
cv .reachableFrom x9
by Lm16;
hence
contradiction
by A13, A32, A31;
verum end; then consider a being
Vertex of
C,
e being
set such that A33:
e Joins cv,
a,
G
;
A34:
e in the_Edges_of G
by A33, GLIB_000:def 13;
now ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )per cases
( C is _trivial or not C is _trivial )
;
suppose
C is
_trivial
;
ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )then consider v99 being
Vertex of
C such that A35:
the_Vertices_of C = {v99}
by GLIB_000:22;
the_Vertices_of C c= the_Vertices_of the
removeVertex of
G,
cv
;
then reconsider v9 =
v99 as
Vertex of the
removeVertex of
G,
cv ;
reconsider v =
v9 as
Vertex of
G by GLIB_000:42;
take v =
v;
( v in the_Vertices_of C & not v is cut-vertex )thus
v in the_Vertices_of C
;
not v is cut-vertex
not
v9 in {cv}
by A9, XBOOLE_0:def 5;
then A36:
v9 <> cv
by TARSKI:def 1;
A37:
{v9} = the
removeVertex of
G,
cv .reachableFrom v9
by A35, Lm16;
now not v is cut-vertex set G3 = the
removeVertex of
G,
v;
A38:
now for e, z being set holds
( not e Joins v,z,G or z = v or z = cv )let e,
z be
set ;
( not e Joins v,z,G or z = v or z = cv )assume A39:
e Joins v,
z,
G
;
( z = v or z = cv )then A40:
e in the_Edges_of G
by GLIB_000:def 13;
now ( z <> v implies not z <> cv )assume that A41:
z <> v
and A42:
z <> cv
;
contradiction
not
e in cv .edgesInOut()
by A36, A39, A42, GLIB_000:65;
then
e in the_Edges_of the
removeVertex of
G,
cv
by A10, A40, XBOOLE_0:def 5;
then
e Joins v,
z, the
removeVertex of
G,
cv
by A39, GLIB_000:73;
then
z in the
removeVertex of
G,
cv .reachableFrom v9
by Lm1, Lm2;
hence
contradiction
by A37, A41, TARSKI:def 1;
verum end; hence
(
z = v or
z = cv )
;
verum end; now for x, y being Vertex of the removeVertex of G,v ex P being Walk of the removeVertex of G,v st P is_Walk_from x,ylet x,
y be
Vertex of the
removeVertex of
G,
v;
ex P being Walk of the removeVertex of G,v st P is_Walk_from x,ynow ex W being Walk of the removeVertex of G,v st W is_Walk_from x,yper cases
( x = y or x <> y )
;
suppose A44:
x <> y
;
ex P being Walk of the removeVertex of G,v st P is_Walk_from x,yreconsider x9 =
x,
y9 =
y as
Vertex of
G by GLIB_000:42;
consider W being
Walk of
G such that A45:
W is_Walk_from x9,
y9
by Def1;
set P = the
Path of
W;
A46:
the
Path of
W is_Walk_from x9,
y9
by A45, GLIB_001:160;
A47:
the_Vertices_of the
removeVertex of
G,
v = (the_Vertices_of G) \ {v}
by GLIB_000:47;
then
not
x in {v}
by XBOOLE_0:def 5;
then
x <> v
by TARSKI:def 1;
then A48:
v <> the
Path of
W . 1
by A46, GLIB_001:17;
not
y in {v}
by A47, XBOOLE_0:def 5;
then
y <> v
by TARSKI:def 1;
then A49:
v <> the
Path of
W . (len the Path of W)
by A46, GLIB_001:17;
now not v in the Path of W .vertices() assume
v in the
Path of
W .vertices()
;
contradictionthen consider n being
odd Element of
NAT such that A50:
n <= len the
Path of
W
and A51:
the
Path of
W . n = v
by GLIB_001:87;
1
<= n
by ABIAN:12;
then
1
< n
by A48, A51, XXREAL_0:1;
then
1
+ 1
<= n
by NAT_1:13;
then reconsider n2 =
n - (2 * 1) as
odd Element of
NAT by INT_1:5;
set e1 = the
Path of
W . (n2 + 1);
set e2 = the
Path of
W . (n + 1);
n - 2
< (len the Path of W) - 0
by A50, XREAL_1:15;
then
the
Path of
W . (n2 + 1) Joins the
Path of
W . n2, the
Path of
W . (n2 + 2),
G
by GLIB_001:def 3;
then A54:
the
Path of
W . n2 = cv
by A38, A51, A52, GLIB_000:14;
A55:
n < len the
Path of
W
by A49, A50, A51, XXREAL_0:1;
then A56:
n + 2
<= len the
Path of
W
by GLIB_001:1;
n2 < n - 0
by XREAL_1:15;
then A59:
n2 + 0 < n + 2
by XREAL_1:8;
the
Path of
W . (n + 1) Joins v, the
Path of
W . (n + 2),
G
by A51, A55, GLIB_001:def 3;
then A60:
the
Path of
W . (n + 2) = cv
by A38, A57;
then
cv = the
Path of
W . 1
by A54, A56, A59, GLIB_001:def 28;
then A61:
cv = x
by A46, GLIB_001:17;
cv = the
Path of
W . (len the Path of W)
by A54, A56, A60, A59, GLIB_001:def 28;
hence
contradiction
by A44, A46, A61, GLIB_001:17;
verum end; then reconsider P = the
Path of
W as
Walk of the
removeVertex of
G,
v by GLIB_001:171;
take P =
P;
P is_Walk_from x,ythus
P is_Walk_from x,
y
by A46, GLIB_001:19;
verum end; hence
ex
P being
Walk of the
removeVertex of
G,
v st
P is_Walk_from x,
y
;
verum end; then A62:
the
removeVertex of
G,
v is
connected
;
assume
v is
cut-vertex
;
contradictionthen
1
< the
removeVertex of
G,
v .numComponents()
by A3;
hence
contradiction
by A62, Lm18;
verum end; hence
not
v is
cut-vertex
;
verum end; suppose
not
C is
_trivial
;
ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )then reconsider C9 =
C as non
_trivial _Graph ;
(C .order()) + 0 < ( the removeVertex of G,cv .order()) + 1
by GLIB_000:75, XREAL_1:8;
then consider v1,
v2 being
Vertex of
C9 such that A63:
v1 <> v2
and A64:
not
v1 is
cut-vertex
and A65:
not
v2 is
cut-vertex
by A1, A11;
set C9R1 = the
removeVertex of
C9,
v1;
A66:
the
removeVertex of
C9,
v1 is
connected
by A64, Lm20;
set C9R2 = the
removeVertex of
C9,
v2;
A67:
the_Vertices_of the
removeVertex of
C9,
v1 = (the_Vertices_of C9) \ {v1}
by GLIB_000:47;
v2 in the_Vertices_of the
removeVertex of
G,
cv
by GLIB_000:42;
then
not
v2 in {cv}
by A9, XBOOLE_0:def 5;
then A68:
v2 <> cv
by TARSKI:def 1;
A69:
the_Vertices_of the
removeVertex of
C9,
v2 = (the_Vertices_of C9) \ {v2}
by GLIB_000:47;
v1 in the_Vertices_of the
removeVertex of
G,
cv
by GLIB_000:42;
then
not
v1 in {cv}
by A9, XBOOLE_0:def 5;
then A70:
v1 <> cv
by TARSKI:def 1;
A71:
the
removeVertex of
C9,
v2 is
connected
by A65, Lm20;
now ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )per cases
( not v1 in cv .allNeighbors() or ( v1 in cv .allNeighbors() & not v2 in cv .allNeighbors() ) or ( v1 in cv .allNeighbors() & v2 in cv .allNeighbors() ) )
;
suppose A72:
not
v1 in cv .allNeighbors()
;
ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )reconsider v9 =
v1 as
Vertex of the
removeVertex of
G,
cv by GLIB_000:42;
reconsider v =
v9 as
Vertex of
G by GLIB_000:42;
take v =
v;
( v in the_Vertices_of C & not v is cut-vertex )thus
v in the_Vertices_of C
;
not v is cut-vertex set G3 = the
removeVertex of
G,
v;
A73:
the_Vertices_of the
removeVertex of
G,
v = (the_Vertices_of G) \ {v}
by GLIB_000:47;
not
cv in {v}
by A70, TARSKI:def 1;
then reconsider cv9 =
cv as
Vertex of the
removeVertex of
G,
v by A73, XBOOLE_0:def 5;
A74:
v1 <> a
by A33, A72, GLIB_000:71;
A75:
the_Vertices_of C = the
removeVertex of
G,
cv .reachableFrom v9
by Lm16;
now for y being Vertex of the removeVertex of G,v ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,ylet y be
Vertex of the
removeVertex of
G,
v;
ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,ynow ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,yper cases
( y = cv or y <> cv )
;
suppose A76:
y <> cv
;
ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,ynow ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,yper cases
( y in the_Vertices_of C or not y in the_Vertices_of C )
;
suppose A77:
y in the_Vertices_of C
;
ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
not
a in {v1}
by A74, TARSKI:def 1;
then A78:
a in the_Vertices_of the
removeVertex of
C9,
v1
by A67, XBOOLE_0:def 5;
not
y in {v1}
by A73, XBOOLE_0:def 5;
then
y in the_Vertices_of the
removeVertex of
C9,
v1
by A67, A77, XBOOLE_0:def 5;
then consider W being
Walk of the
removeVertex of
C9,
v1 such that A79:
W is_Walk_from y,
a
by A66, A78;
A80:
(
W . 1
= y &
W . (len W) = a )
by A79, GLIB_001:17;
not
e in v .edgesInOut()
by A33, A70, A74, GLIB_000:65;
then
e in (the_Edges_of G) \ (v .edgesInOut())
by A34, XBOOLE_0:def 5;
then
e in (the_Edges_of G) \ (G .edgesInOut {v})
by GLIB_000:def 40;
then
e in G .edgesBetween ((the_Vertices_of G) \ {v})
by GLIB_000:35;
then
e in the_Edges_of the
removeVertex of
G,
v
by GLIB_000:47;
then
e Joins cv,
a, the
removeVertex of
G,
v
by A33, GLIB_000:73;
then A82:
e Joins a,
cv, the
removeVertex of
G,
v
by GLIB_000:14;
reconsider W =
W as
Walk of
C by GLIB_001:167;
reconsider W =
W as
Walk of the
removeVertex of
G,
cv by GLIB_001:167;
reconsider W =
W as
Walk of
G by GLIB_001:167;
not
v in W .vertices()
by A81, GLIB_001:98;
then reconsider W =
W as
Walk of the
removeVertex of
G,
v by GLIB_001:171;
W is_Walk_from y,
a
by A80, GLIB_001:17;
then
W .addEdge e is_Walk_from y,
cv
by A82, GLIB_001:66;
then
(W .addEdge e) .reverse() is_Walk_from cv,
y
by GLIB_001:23;
hence
ex
W being
Walk of the
removeVertex of
G,
v st
W is_Walk_from cv9,
y
;
verum suppose A83:
not
y in the_Vertices_of C
;
ex P being Walk of the removeVertex of G,v st P is_Walk_from cv9,yreconsider y9 =
y as
Vertex of
G by GLIB_000:42;
consider W being
Walk of
G such that A84:
W is_Walk_from cv,
y9
by Def1;
set P = the
Path of
W;
A85:
the
Path of
W is_Walk_from cv,
y9
by A84, GLIB_001:160;
then A86:
the
Path of
W . (len the Path of W) = y9
by GLIB_001:17;
A87:
the
Path of
W . 1
= cv
by A85, GLIB_001:17;
now not v in the Path of W .vertices() assume
v in the
Path of
W .vertices()
;
contradictionthen consider n being
odd Element of
NAT such that A88:
n <= len the
Path of
W
and A89:
the
Path of
W . n = v
by GLIB_001:87;
set P2 = the
Path of
W .cut (
n,
(len the Path of W));
A90:
the
Path of
W .cut (
n,
(len the Path of W))
is_Walk_from v,
y9
by A86, A88, A89, GLIB_001:37;
1
<= n
by ABIAN:12;
then A91:
1
< n
by A70, A87, A89, XXREAL_0:1;
now not cv in ( the Path of W .cut (n,(len the Path of W))) .vertices() assume
cv in ( the Path of W .cut (n,(len the Path of W))) .vertices()
;
contradictionthen consider m being
odd Element of
NAT such that A92:
m <= len ( the Path of W .cut (n,(len the Path of W)))
and A93:
( the Path of W .cut (n,(len the Path of W))) . m = cv
by GLIB_001:87;
1
<= m
by ABIAN:12;
then A94:
m in dom ( the Path of W .cut (n,(len the Path of W)))
by A92, FINSEQ_3:25;
then A95:
the
Path of
W . ((n + m) - 1) = cv
by A88, A93, GLIB_001:47;
1
+ 1
< n + m
by A91, ABIAN:12, XREAL_1:8;
then
(1 + 1) - 1
< (n + m) - 1
by XREAL_1:14;
then A96:
(2 * 0) + 1
< (n + m) - 1
;
A97:
(n + m) - 1
in dom the
Path of
W
by A88, A94, GLIB_001:47;
then
(n + m) - 1
<= len the
Path of
W
by FINSEQ_3:25;
hence
contradiction
by A76, A87, A86, A95, A97, A96, GLIB_001:def 28;
verum end; then reconsider P2 = the
Path of
W .cut (
n,
(len the Path of W)) as
Walk of the
removeVertex of
G,
cv by GLIB_001:171;
P2 is_Walk_from v,
y9
by A90, GLIB_001:19;
hence
contradiction
by A75, A83, Def5;
verum end; then reconsider P = the
Path of
W as
Walk of the
removeVertex of
G,
v by GLIB_001:171;
take P =
P;
P is_Walk_from cv9,ythus
P is_Walk_from cv9,
y
by A85, GLIB_001:19;
verum end; hence
ex
W being
Walk of the
removeVertex of
G,
v st
W is_Walk_from cv9,
y
;
verum hence
ex
W being
Walk of the
removeVertex of
G,
v st
W is_Walk_from cv9,
y
;
verum end; then
the
removeVertex of
G,
v is
connected
by Lm6;
then
the
removeVertex of
G,
v .numComponents() = 1
by Lm18;
hence
not
v is
cut-vertex
by A3;
verum end; suppose A98:
(
v1 in cv .allNeighbors() & not
v2 in cv .allNeighbors() )
;
ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )reconsider v9 =
v2 as
Vertex of the
removeVertex of
G,
cv by GLIB_000:42;
reconsider v =
v9 as
Vertex of
G by GLIB_000:42;
take v =
v;
( v in the_Vertices_of C & not v is cut-vertex )thus
v in the_Vertices_of C
;
not v is cut-vertex set G3 = the
removeVertex of
G,
v;
A99:
the_Vertices_of the
removeVertex of
G,
v = (the_Vertices_of G) \ {v}
by GLIB_000:47;
not
cv in {v}
by A68, TARSKI:def 1;
then reconsider cv9 =
cv as
Vertex of the
removeVertex of
G,
v by A99, XBOOLE_0:def 5;
A100:
v2 <> a
by A33, A98, GLIB_000:71;
A101:
the_Vertices_of C = the
removeVertex of
G,
cv .reachableFrom v9
by Lm16;
now for y being Vertex of the removeVertex of G,v ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,ylet y be
Vertex of the
removeVertex of
G,
v;
ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,ynow ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,yper cases
( y = cv or y <> cv )
;
suppose A102:
y <> cv
;
ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,ynow ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,yper cases
( y in the_Vertices_of C or not y in the_Vertices_of C )
;
suppose A103:
y in the_Vertices_of C
;
ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
not
a in {v2}
by A100, TARSKI:def 1;
then A104:
a in the_Vertices_of the
removeVertex of
C9,
v2
by A69, XBOOLE_0:def 5;
not
y in {v2}
by A99, XBOOLE_0:def 5;
then
y in the_Vertices_of the
removeVertex of
C9,
v2
by A69, A103, XBOOLE_0:def 5;
then consider W being
Walk of the
removeVertex of
C9,
v2 such that A105:
W is_Walk_from y,
a
by A71, A104;
A106:
(
W . 1
= y &
W . (len W) = a )
by A105, GLIB_001:17;
not
e in v .edgesInOut()
by A33, A68, A100, GLIB_000:65;
then
e in (the_Edges_of G) \ (v .edgesInOut())
by A34, XBOOLE_0:def 5;
then
e in (the_Edges_of G) \ (G .edgesInOut {v})
by GLIB_000:def 40;
then
e in G .edgesBetween ((the_Vertices_of G) \ {v})
by GLIB_000:35;
then
e in the_Edges_of the
removeVertex of
G,
v
by GLIB_000:47;
then
e Joins cv,
a, the
removeVertex of
G,
v
by A33, GLIB_000:73;
then A108:
e Joins a,
cv, the
removeVertex of
G,
v
by GLIB_000:14;
reconsider W =
W as
Walk of
C by GLIB_001:167;
reconsider W =
W as
Walk of the
removeVertex of
G,
cv by GLIB_001:167;
reconsider W =
W as
Walk of
G by GLIB_001:167;
not
v in W .vertices()
by A107, GLIB_001:98;
then reconsider W =
W as
Walk of the
removeVertex of
G,
v by GLIB_001:171;
W is_Walk_from y,
a
by A106, GLIB_001:17;
then
W .addEdge e is_Walk_from y,
cv
by A108, GLIB_001:66;
then
(W .addEdge e) .reverse() is_Walk_from cv,
y
by GLIB_001:23;
hence
ex
W being
Walk of the
removeVertex of
G,
v st
W is_Walk_from cv9,
y
;
verum suppose A109:
not
y in the_Vertices_of C
;
ex P being Walk of the removeVertex of G,v st P is_Walk_from cv9,yreconsider y9 =
y as
Vertex of
G by GLIB_000:42;
consider W being
Walk of
G such that A110:
W is_Walk_from cv,
y9
by Def1;
set P = the
Path of
W;
A111:
the
Path of
W is_Walk_from cv,
y9
by A110, GLIB_001:160;
then A112:
the
Path of
W . (len the Path of W) = y9
by GLIB_001:17;
A113:
the
Path of
W . 1
= cv
by A111, GLIB_001:17;
now not v in the Path of W .vertices() assume
v in the
Path of
W .vertices()
;
contradictionthen consider n being
odd Element of
NAT such that A114:
n <= len the
Path of
W
and A115:
the
Path of
W . n = v
by GLIB_001:87;
set P2 = the
Path of
W .cut (
n,
(len the Path of W));
A116:
the
Path of
W .cut (
n,
(len the Path of W))
is_Walk_from v,
y9
by A112, A114, A115, GLIB_001:37;
1
<= n
by ABIAN:12;
then A117:
1
< n
by A68, A113, A115, XXREAL_0:1;
now not cv in ( the Path of W .cut (n,(len the Path of W))) .vertices() assume
cv in ( the Path of W .cut (n,(len the Path of W))) .vertices()
;
contradictionthen consider m being
odd Element of
NAT such that A118:
m <= len ( the Path of W .cut (n,(len the Path of W)))
and A119:
( the Path of W .cut (n,(len the Path of W))) . m = cv
by GLIB_001:87;
1
<= m
by ABIAN:12;
then A120:
m in dom ( the Path of W .cut (n,(len the Path of W)))
by A118, FINSEQ_3:25;
then A121:
the
Path of
W . ((n + m) - 1) = cv
by A114, A119, GLIB_001:47;
1
+ 1
< n + m
by A117, ABIAN:12, XREAL_1:8;
then
(1 + 1) - 1
< (n + m) - 1
by XREAL_1:14;
then A122:
(2 * 0) + 1
< (n + m) - 1
;
A123:
(n + m) - 1
in dom the
Path of
W
by A114, A120, GLIB_001:47;
then
(n + m) - 1
<= len the
Path of
W
by FINSEQ_3:25;
hence
contradiction
by A102, A113, A112, A121, A123, A122, GLIB_001:def 28;
verum end; then reconsider P2 = the
Path of
W .cut (
n,
(len the Path of W)) as
Walk of the
removeVertex of
G,
cv by GLIB_001:171;
P2 is_Walk_from v,
y9
by A116, GLIB_001:19;
hence
contradiction
by A101, A109, Def5;
verum end; then reconsider P = the
Path of
W as
Walk of the
removeVertex of
G,
v by GLIB_001:171;
take P =
P;
P is_Walk_from cv9,ythus
P is_Walk_from cv9,
y
by A111, GLIB_001:19;
verum end; hence
ex
W being
Walk of the
removeVertex of
G,
v st
W is_Walk_from cv9,
y
;
verum hence
ex
W being
Walk of the
removeVertex of
G,
v st
W is_Walk_from cv9,
y
;
verum end; then
the
removeVertex of
G,
v is
connected
by Lm6;
then
the
removeVertex of
G,
v .numComponents() = 1
by Lm18;
hence
not
v is
cut-vertex
by A3;
verum end; suppose
(
v1 in cv .allNeighbors() &
v2 in cv .allNeighbors() )
;
ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )then consider e being
object such that A124:
e Joins cv,
v2,
G
by GLIB_000:71;
reconsider v9 =
v1 as
Vertex of the
removeVertex of
G,
cv by GLIB_000:42;
set a =
v2;
reconsider v =
v9 as
Vertex of
G by GLIB_000:42;
take v =
v;
( v in the_Vertices_of C & not v is cut-vertex )thus
v in the_Vertices_of C
;
not v is cut-vertex set G3 = the
removeVertex of
G,
v;
A125:
the_Vertices_of the
removeVertex of
G,
v = (the_Vertices_of G) \ {v}
by GLIB_000:47;
not
cv in {v}
by A70, TARSKI:def 1;
then reconsider cv9 =
cv as
Vertex of the
removeVertex of
G,
v by A125, XBOOLE_0:def 5;
A126:
the_Vertices_of C = the
removeVertex of
G,
cv .reachableFrom v9
by Lm16;
A127:
e in the_Edges_of G
by A124, GLIB_000:def 13;
now for y being Vertex of the removeVertex of G,v ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,ylet y be
Vertex of the
removeVertex of
G,
v;
ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,ynow ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,yper cases
( y = cv or y <> cv )
;
suppose A128:
y <> cv
;
ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,ynow ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,yper cases
( y in the_Vertices_of C or not y in the_Vertices_of C )
;
suppose A129:
y in the_Vertices_of C
;
ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
not
v2 in {v1}
by A63, TARSKI:def 1;
then A130:
v2 in the_Vertices_of the
removeVertex of
C9,
v1
by A67, XBOOLE_0:def 5;
not
y in {v1}
by A125, XBOOLE_0:def 5;
then
y in the_Vertices_of the
removeVertex of
C9,
v1
by A67, A129, XBOOLE_0:def 5;
then consider W being
Walk of the
removeVertex of
C9,
v1 such that A131:
W is_Walk_from y,
v2
by A66, A130;
A132:
(
W . 1
= y &
W . (len W) = v2 )
by A131, GLIB_001:17;
not
e in v .edgesInOut()
by A63, A70, A124, GLIB_000:65;
then
e in (the_Edges_of G) \ (v .edgesInOut())
by A127, XBOOLE_0:def 5;
then
e in (the_Edges_of G) \ (G .edgesInOut {v})
by GLIB_000:def 40;
then
e in G .edgesBetween ((the_Vertices_of G) \ {v})
by GLIB_000:35;
then
e in the_Edges_of the
removeVertex of
G,
v
by GLIB_000:47;
then
e Joins cv,
v2, the
removeVertex of
G,
v
by A124, GLIB_000:73;
then A134:
e Joins v2,
cv, the
removeVertex of
G,
v
by GLIB_000:14;
reconsider W =
W as
Walk of
C by GLIB_001:167;
reconsider W =
W as
Walk of the
removeVertex of
G,
cv by GLIB_001:167;
reconsider W =
W as
Walk of
G by GLIB_001:167;
not
v in W .vertices()
by A133, GLIB_001:98;
then reconsider W =
W as
Walk of the
removeVertex of
G,
v by GLIB_001:171;
W is_Walk_from y,
v2
by A132, GLIB_001:17;
then
W .addEdge e is_Walk_from y,
cv
by A134, GLIB_001:66;
then
(W .addEdge e) .reverse() is_Walk_from cv,
y
by GLIB_001:23;
hence
ex
W being
Walk of the
removeVertex of
G,
v st
W is_Walk_from cv9,
y
;
verum suppose A135:
not
y in the_Vertices_of C
;
ex P being Walk of the removeVertex of G,v st P is_Walk_from cv9,yreconsider y9 =
y as
Vertex of
G by GLIB_000:42;
consider W being
Walk of
G such that A136:
W is_Walk_from cv,
y9
by Def1;
set P = the
Path of
W;
A137:
the
Path of
W is_Walk_from cv,
y9
by A136, GLIB_001:160;
then A138:
the
Path of
W . (len the Path of W) = y9
by GLIB_001:17;
A139:
the
Path of
W . 1
= cv
by A137, GLIB_001:17;
now not v in the Path of W .vertices() assume
v in the
Path of
W .vertices()
;
contradictionthen consider n being
odd Element of
NAT such that A140:
n <= len the
Path of
W
and A141:
the
Path of
W . n = v
by GLIB_001:87;
set P2 = the
Path of
W .cut (
n,
(len the Path of W));
A142:
the
Path of
W .cut (
n,
(len the Path of W))
is_Walk_from v,
y9
by A138, A140, A141, GLIB_001:37;
1
<= n
by ABIAN:12;
then A143:
1
< n
by A70, A139, A141, XXREAL_0:1;
now not cv in ( the Path of W .cut (n,(len the Path of W))) .vertices() assume
cv in ( the Path of W .cut (n,(len the Path of W))) .vertices()
;
contradictionthen consider m being
odd Element of
NAT such that A144:
m <= len ( the Path of W .cut (n,(len the Path of W)))
and A145:
( the Path of W .cut (n,(len the Path of W))) . m = cv
by GLIB_001:87;
1
<= m
by ABIAN:12;
then A146:
m in dom ( the Path of W .cut (n,(len the Path of W)))
by A144, FINSEQ_3:25;
then A147:
the
Path of
W . ((n + m) - 1) = cv
by A140, A145, GLIB_001:47;
1
+ 1
< n + m
by A143, ABIAN:12, XREAL_1:8;
then
(1 + 1) - 1
< (n + m) - 1
by XREAL_1:14;
then A148:
(2 * 0) + 1
< (n + m) - 1
;
A149:
(n + m) - 1
in dom the
Path of
W
by A140, A146, GLIB_001:47;
then
(n + m) - 1
<= len the
Path of
W
by FINSEQ_3:25;
hence
contradiction
by A128, A139, A138, A147, A149, A148, GLIB_001:def 28;
verum end; then reconsider P2 = the
Path of
W .cut (
n,
(len the Path of W)) as
Walk of the
removeVertex of
G,
cv by GLIB_001:171;
P2 is_Walk_from v,
y9
by A142, GLIB_001:19;
hence
contradiction
by A126, A135, Def5;
verum end; then reconsider P = the
Path of
W as
Walk of the
removeVertex of
G,
v by GLIB_001:171;
take P =
P;
P is_Walk_from cv9,ythus
P is_Walk_from cv9,
y
by A137, GLIB_001:19;
verum end; hence
ex
W being
Walk of the
removeVertex of
G,
v st
W is_Walk_from cv9,
y
;
verum hence
ex
W being
Walk of the
removeVertex of
G,
v st
W is_Walk_from cv9,
y
;
verum end; then
the
removeVertex of
G,
v is
connected
by Lm6;
then
the
removeVertex of
G,
v .numComponents() = 1
by Lm18;
hence
not
v is
cut-vertex
by A3;
verum end; hence
ex
v being
Vertex of
G st
(
v in the_Vertices_of C & not
v is
cut-vertex )
;
verum end; hence
ex
v being
Vertex of
G st
(
v in the_Vertices_of C & not
v is
cut-vertex )
;
verum end; then consider v1 being
Vertex of
G such that A150:
v1 in the_Vertices_of the
inducedSubgraph of the
removeVertex of
G,
cv,
C1
and A151:
not
v1 is
cut-vertex
;
consider v2 being
Vertex of
G such that A152:
v2 in the_Vertices_of the
inducedSubgraph of the
removeVertex of
G,
cv,
C2
and A153:
not
v2 is
cut-vertex
by A12;
take v1 =
v1;
ex v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )take v2 =
v2;
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )now not v1 = v2
C2 is non
empty Subset of
(the_Vertices_of the removeVertex of G,cv)
by Lm13;
then A154:
the_Vertices_of the
inducedSubgraph of the
removeVertex of
G,
cv,
C2 = C2
by GLIB_000:def 37;
C1 is non
empty Subset of
(the_Vertices_of the removeVertex of G,cv)
by Lm13;
then A155:
the_Vertices_of the
inducedSubgraph of the
removeVertex of
G,
cv,
C1 = C1
by GLIB_000:def 37;
assume
v1 = v2
;
contradictionthen
the
inducedSubgraph of the
removeVertex of
G,
cv,
C1 == the
inducedSubgraph of the
removeVertex of
G,
cv,
C2
by A150, A152, Lm17;
hence
contradiction
by A8, A155, A154, GLIB_000:def 34;
verum end; hence
v1 <> v2
;
( not v1 is cut-vertex & not v2 is cut-vertex )thus
( not
v1 is
cut-vertex & not
v2 is
cut-vertex )
by A151, A153;
verum end; hence
ex
v1,
v2 being
Vertex of
G st
(
v1 <> v2 & not
v1 is
cut-vertex & not
v2 is
cut-vertex )
;
verum end; hence
S1[
k]
;
verum end;
then A156:
for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]
;
A157:
for k being Nat holds S1[k]
from NAT_1:sch 4(A156);
G .order() = G .order()
;
hence
ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )
by A157; verum