let G be finite non trivial connected _Graph; :: thesis: 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 :: thesis: for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]
let k be Nat; :: thesis: ( ( 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] ; :: thesis: S1[k]
now :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 :: thesis: 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 A4: for v being Vertex of G holds not v is cut-vertex ; :: thesis: ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )

consider v1, v2 being Vertex of G such that
A5: v1 <> v2 by GLIB_000:21;
take v1 = v1; :: thesis: ex v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )

take v2 = v2; :: thesis: ( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )
thus v1 <> v2 by A5; :: thesis: ( not v1 is cut-vertex & not v2 is cut-vertex )
thus ( not v1 is cut-vertex & not v2 is cut-vertex ) by A4; :: thesis: verum
end;
suppose ex cv being Vertex of G st cv is cut-vertex ; :: thesis: 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 = () \ {cv} by GLIB_000:47;
G .edgesBetween (() \ {cv}) = () \ () by GLIB_000:35;
then G .edgesBetween (() \ {cv}) = () \ () by GLIB_000:def 40;
then A10: the_Edges_of the removeVertex of G,cv = () \ () by GLIB_000:47;
A11: ( the removeVertex of G,cv .order()) + 1 = k by ;
A12: now :: thesis: 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; :: thesis: ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )

now :: thesis: ex a being Vertex of C ex e being set st e Joins cv,a,G
set x = the Vertex of C;
assume A13: for a being Vertex of C
for e being set holds not e Joins cv,a,G ; :: thesis: 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 ;
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 ;
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 ;
then A20: the Vertex of C <> cv by TARSKI:def 1;
then A21: not the Path of W is trivial by ;
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 ;
A24: the Path of W . ((2 * 0) + 1) = cv by ;
now :: thesis: 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() ; :: thesis: contradiction
then 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 ;
then (3 + n) - 1 in dom the Path of W by ;
then A30: 2 + n <= len the Path of W by FINSEQ_3:25;
the Path of W . ((3 + n) - 1) = cv by ;
hence contradiction by A20, A24, A19, A30, A28, GLIB_001:def 28; :: thesis: 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 ;
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 ;
then (2 * 0) + 1 < len the Path of W by ;
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 ;
the_Vertices_of C = the removeVertex of G,cv .reachableFrom x9 by Lm16;
hence contradiction by A13, A32, A31; :: thesis: 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 ;
now :: thesis: 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 ; :: thesis: 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; :: thesis: ( v in the_Vertices_of C & not v is cut-vertex )
thus v in the_Vertices_of C ; :: thesis: not v is cut-vertex
not v9 in {cv} by ;
then A36: v9 <> cv by TARSKI:def 1;
A37: {v9} = the removeVertex of G,cv .reachableFrom v9 by ;
now :: thesis: not v is cut-vertex
set G3 = the removeVertex of G,v;
A38: now :: thesis: for e, z being set holds
( not e Joins v,z,G or z = v or z = cv )
let e, z be set ; :: thesis: ( not e Joins v,z,G or z = v or z = cv )
assume A39: e Joins v,z,G ; :: thesis: ( z = v or z = cv )
then A40: e in the_Edges_of G by GLIB_000:def 13;
now :: thesis: ( z <> v implies not z <> cv )
assume that
A41: z <> v and
A42: z <> cv ; :: thesis: contradiction
not e in cv .edgesInOut() by ;
then e in the_Edges_of the removeVertex of G,cv by ;
then e Joins v,z, the removeVertex of G,cv by ;
then z in the removeVertex of G,cv .reachableFrom v9 by ;
hence contradiction by A37, A41, TARSKI:def 1; :: thesis: verum
end;
hence ( z = v or z = cv ) ; :: thesis: verum
end;
now :: thesis: 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,y
let x, y be Vertex of the removeVertex of G,v; :: thesis: ex P being Walk of the removeVertex of G,v st P is_Walk_from x,y
now :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from x,y
per cases ( x = y or x <> y ) ;
suppose A43: x = y ; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from x,y
set W = the removeVertex of G,v .walkOf x;
take W = the removeVertex of G,v .walkOf x; :: thesis: W is_Walk_from x,y
thus W is_Walk_from x,y by ; :: thesis: verum
end;
suppose A44: x <> y ; :: thesis: ex P being Walk of the removeVertex of G,v st P is_Walk_from x,y
reconsider 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 ;
A47: the_Vertices_of the removeVertex of G,v = () \ {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 ;
not y in {v} by ;
then y <> v by TARSKI:def 1;
then A49: v <> the Path of W . (len the Path of W) by ;
now :: thesis: not v in the Path of W .vertices()
assume v in the Path of W .vertices() ; :: thesis: contradiction
then 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 ;
then 1 + 1 <= n by NAT_1:13;
then reconsider n2 = n - (2 * 1) as odd Element of NAT by INT_1:5;
A52: now :: thesis: not the Path of W . n2 = vend;
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 ;
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 ;
A55: n < len the Path of W by ;
then A56: n + 2 <= len the Path of W by GLIB_001:1;
A57: now :: thesis: not the Path of W . (n + 2) = v
A58: n + 0 < n + 2 by XREAL_1:8;
assume the Path of W . (n + 2) = v ; :: thesis: contradiction
hence contradiction by A48, A51, A56, A58, GLIB_001:def 28; :: thesis: verum
end;
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 ;
then A60: the Path of W . (n + 2) = cv by ;
then cv = the Path of W . 1 by ;
then A61: cv = x by ;
cv = the Path of W . (len the Path of W) by ;
hence contradiction by A44, A46, A61, GLIB_001:17; :: thesis: verum
end;
then reconsider P = the Path of W as Walk of the removeVertex of G,v by GLIB_001:171;
take P = P; :: thesis: P is_Walk_from x,y
thus P is_Walk_from x,y by ; :: thesis: verum
end;
end;
end;
hence ex P being Walk of the removeVertex of G,v st P is_Walk_from x,y ; :: thesis: verum
end;
then A62: the removeVertex of G,v is connected ;
assume v is cut-vertex ; :: thesis: contradiction
then 1 < the removeVertex of G,v .numComponents() by A3;
hence contradiction by A62, Lm18; :: thesis: verum
end;
hence not v is cut-vertex ; :: thesis: verum
end;
suppose not C is trivial ; :: thesis: 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 ;
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 ;
set C9R1 = the removeVertex of C9,v1;
A66: the removeVertex of C9,v1 is connected by ;
set C9R2 = the removeVertex of C9,v2;
A67: the_Vertices_of the removeVertex of C9,v1 = () \ {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 ;
then A68: v2 <> cv by TARSKI:def 1;
A69: the_Vertices_of the removeVertex of C9,v2 = () \ {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 ;
then A70: v1 <> cv by TARSKI:def 1;
A71: the removeVertex of C9,v2 is connected by ;
now :: thesis: 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() ; :: thesis: 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; :: thesis: ( v in the_Vertices_of C & not v is cut-vertex )
thus v in the_Vertices_of C ; :: thesis: not v is cut-vertex
set G3 = the removeVertex of G,v;
A73: the_Vertices_of the removeVertex of G,v = () \ {v} by GLIB_000:47;
not cv in {v} by ;
then reconsider cv9 = cv as Vertex of the removeVertex of G,v by ;
A74: v1 <> a by ;
A75: the_Vertices_of C = the removeVertex of G,cv .reachableFrom v9 by Lm16;
now :: thesis: 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,y
let y be Vertex of the removeVertex of G,v; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
now :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
per cases ( y = cv or y <> cv ) ;
suppose y = cv ; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
end;
suppose A76: y <> cv ; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
now :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
per cases ( y in the_Vertices_of C or not y in the_Vertices_of C ) ;
suppose A77: y in the_Vertices_of C ; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
not a in {v1} by ;
then A78: a in the_Vertices_of the removeVertex of C9,v1 by ;
not y in {v1} by ;
then y in the_Vertices_of the removeVertex of C9,v1 by ;
then consider W being Walk of the removeVertex of C9,v1 such that
A79: W is_Walk_from y,a by ;
A80: ( W . 1 = y & W . (len W) = a ) by ;
not e in v .edgesInOut() by ;
then e in () \ () by ;
then e in () \ () by GLIB_000:def 40;
then e in G .edgesBetween (() \ {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 ;
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 ;
then reconsider W = W as Walk of the removeVertex of G,v by GLIB_001:171;
W is_Walk_from y,a by ;
then W .addEdge e is_Walk_from y,cv by ;
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 ; :: thesis: verum
end;
suppose A83: not y in the_Vertices_of C ; :: thesis: ex P being Walk of the removeVertex of G,v st P is_Walk_from cv9,y
reconsider 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 ;
then A86: the Path of W . (len the Path of W) = y9 by GLIB_001:17;
A87: the Path of W . 1 = cv by ;
now :: thesis: not v in the Path of W .vertices()
assume v in the Path of W .vertices() ; :: thesis: contradiction
then 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 ;
1 <= n by ABIAN:12;
then A91: 1 < n by ;
now :: thesis: 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() ; :: thesis: contradiction
then 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 ;
then A95: the Path of W . ((n + m) - 1) = cv by ;
1 + 1 < n + m by ;
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 ;
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; :: thesis: 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 ;
hence contradiction by A75, A83, Def5; :: thesis: verum
end;
then reconsider P = the Path of W as Walk of the removeVertex of G,v by GLIB_001:171;
take P = P; :: thesis: P is_Walk_from cv9,y
thus P is_Walk_from cv9,y by ; :: thesis: verum
end;
end;
end;
hence ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; :: thesis: verum
end;
end;
end;
hence ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; :: thesis: 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; :: thesis: verum
end;
suppose A98: ( v1 in cv .allNeighbors() & not v2 in cv .allNeighbors() ) ; :: thesis: 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; :: thesis: ( v in the_Vertices_of C & not v is cut-vertex )
thus v in the_Vertices_of C ; :: thesis: not v is cut-vertex
set G3 = the removeVertex of G,v;
A99: the_Vertices_of the removeVertex of G,v = () \ {v} by GLIB_000:47;
not cv in {v} by ;
then reconsider cv9 = cv as Vertex of the removeVertex of G,v by ;
A100: v2 <> a by ;
A101: the_Vertices_of C = the removeVertex of G,cv .reachableFrom v9 by Lm16;
now :: thesis: 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,y
let y be Vertex of the removeVertex of G,v; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
now :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
per cases ( y = cv or y <> cv ) ;
suppose y = cv ; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
end;
suppose A102: y <> cv ; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
now :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
per cases ( y in the_Vertices_of C or not y in the_Vertices_of C ) ;
suppose A103: y in the_Vertices_of C ; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
not a in {v2} by ;
then A104: a in the_Vertices_of the removeVertex of C9,v2 by ;
not y in {v2} by ;
then y in the_Vertices_of the removeVertex of C9,v2 by ;
then consider W being Walk of the removeVertex of C9,v2 such that
A105: W is_Walk_from y,a by ;
A106: ( W . 1 = y & W . (len W) = a ) by ;
not e in v .edgesInOut() by ;
then e in () \ () by ;
then e in () \ () by GLIB_000:def 40;
then e in G .edgesBetween (() \ {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 ;
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 ;
then reconsider W = W as Walk of the removeVertex of G,v by GLIB_001:171;
W is_Walk_from y,a by ;
then W .addEdge e is_Walk_from y,cv by ;
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 ; :: thesis: verum
end;
suppose A109: not y in the_Vertices_of C ; :: thesis: ex P being Walk of the removeVertex of G,v st P is_Walk_from cv9,y
reconsider 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 ;
then A112: the Path of W . (len the Path of W) = y9 by GLIB_001:17;
A113: the Path of W . 1 = cv by ;
now :: thesis: not v in the Path of W .vertices()
assume v in the Path of W .vertices() ; :: thesis: contradiction
then 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 ;
1 <= n by ABIAN:12;
then A117: 1 < n by ;
now :: thesis: 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() ; :: thesis: contradiction
then 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 ;
then A121: the Path of W . ((n + m) - 1) = cv by ;
1 + 1 < n + m by ;
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 ;
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; :: thesis: 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 ;
hence contradiction by A101, A109, Def5; :: thesis: verum
end;
then reconsider P = the Path of W as Walk of the removeVertex of G,v by GLIB_001:171;
take P = P; :: thesis: P is_Walk_from cv9,y
thus P is_Walk_from cv9,y by ; :: thesis: verum
end;
end;
end;
hence ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; :: thesis: verum
end;
end;
end;
hence ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; :: thesis: 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; :: thesis: verum
end;
suppose ( v1 in cv .allNeighbors() & v2 in cv .allNeighbors() ) ; :: thesis: 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; :: thesis: ( v in the_Vertices_of C & not v is cut-vertex )
thus v in the_Vertices_of C ; :: thesis: not v is cut-vertex
set G3 = the removeVertex of G,v;
A125: the_Vertices_of the removeVertex of G,v = () \ {v} by GLIB_000:47;
not cv in {v} by ;
then reconsider cv9 = cv as Vertex of the removeVertex of G,v by ;
A126: the_Vertices_of C = the removeVertex of G,cv .reachableFrom v9 by Lm16;
A127: e in the_Edges_of G by ;
now :: thesis: 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,y
let y be Vertex of the removeVertex of G,v; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
now :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
per cases ( y = cv or y <> cv ) ;
suppose y = cv ; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
end;
suppose A128: y <> cv ; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
now :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
per cases ( y in the_Vertices_of C or not y in the_Vertices_of C ) ;
suppose A129: y in the_Vertices_of C ; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
not v2 in {v1} by ;
then A130: v2 in the_Vertices_of the removeVertex of C9,v1 by ;
not y in {v1} by ;
then y in the_Vertices_of the removeVertex of C9,v1 by ;
then consider W being Walk of the removeVertex of C9,v1 such that
A131: W is_Walk_from y,v2 by ;
A132: ( W . 1 = y & W . (len W) = v2 ) by ;
not e in v .edgesInOut() by ;
then e in () \ () by ;
then e in () \ () by GLIB_000:def 40;
then e in G .edgesBetween (() \ {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 ;
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 ;
then reconsider W = W as Walk of the removeVertex of G,v by GLIB_001:171;
W is_Walk_from y,v2 by ;
then W .addEdge e is_Walk_from y,cv by ;
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 ; :: thesis: verum
end;
suppose A135: not y in the_Vertices_of C ; :: thesis: ex P being Walk of the removeVertex of G,v st P is_Walk_from cv9,y
reconsider 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 ;
then A138: the Path of W . (len the Path of W) = y9 by GLIB_001:17;
A139: the Path of W . 1 = cv by ;
now :: thesis: not v in the Path of W .vertices()
assume v in the Path of W .vertices() ; :: thesis: contradiction
then 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 ;
1 <= n by ABIAN:12;
then A143: 1 < n by ;
now :: thesis: 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() ; :: thesis: contradiction
then 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 ;
then A147: the Path of W . ((n + m) - 1) = cv by ;
1 + 1 < n + m by ;
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 ;
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; :: thesis: 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 ;
hence contradiction by A126, A135, Def5; :: thesis: verum
end;
then reconsider P = the Path of W as Walk of the removeVertex of G,v by GLIB_001:171;
take P = P; :: thesis: P is_Walk_from cv9,y
thus P is_Walk_from cv9,y by ; :: thesis: verum
end;
end;
end;
hence ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; :: thesis: verum
end;
end;
end;
hence ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; :: thesis: 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; :: thesis: verum
end;
end;
end;
hence ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex ) ; :: thesis: verum
end;
end;
end;
hence ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex ) ; :: thesis: 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; :: thesis: ex v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )

take v2 = v2; :: thesis: ( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )
hence v1 <> v2 ; :: thesis: ( not v1 is cut-vertex & not v2 is cut-vertex )
thus ( not v1 is cut-vertex & not v2 is cut-vertex ) by ; :: thesis: verum
end;
end;
end;
hence ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex ) ; :: thesis: verum
end;
hence S1[k] ; :: thesis: 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 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; :: thesis: verum