let G be finite non trivial connected _Graph; :: thesis:
defpred S₁[ 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

let k be Nat; :: thesis:
assume A1: for n being Nat st n < k holds
S₁[n] ; :: thesis:

now

let G be finite non trivial connected _Graph; :: thesis:
assume A2: G .order() = k ; :: thesis:
A3: G .numComponents() = 1 by Lm18;

now

per cases ;

suppose A4: for v being Vertex of G holds not v is cut-vertex ; :: thesis:

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

end;

suppose ex cv being Vertex of G st cv is cut-vertex ; :: thesis:

then consider cv being Vertex of G such that
A6: cv is cut-vertex ;
consider G2 being removeVertex of G,cv;
1 < G2 .numComponents() by A3, A6, Def11;
then 1 + 1 <= G2 .numComponents() by NAT_1:13;
then card 2 <= card (G2 .componentSet() ) by CARD_1:def 5;
then card 2 c= card (G2 .componentSet() ) by NAT_1:40;
then 2 c= card (G2 .componentSet() ) by CARD_1:def 5;
then consider C1, C2 being set such that
A7: ( C1 in G2 .componentSet() & C2 in G2 .componentSet() ) and
A8: C1 <> C2 by PENCIL_1:2;
reconsider C1 = C1, C2 = C2 as Element of G2 .componentSet() by A7;
consider CC1 being inducedSubgraph of G2,C1;
consider CC2 being inducedSubgraph of G2,C2;
A9: the_Vertices_of G2 = (the_Vertices_of G) \ {cv} by GLIB_000:50;
G .edgesBetween ((the_Vertices_of G) \ {cv}) = (the_Edges_of G) \ (G .edgesInOut {cv}) by GLIB_000:38;
then G .edgesBetween ((the_Vertices_of G) \ {cv}) = (the_Edges_of G) \ (cv .edgesInOut() ) by GLIB_000:def 42;
then A10: the_Edges_of G2 = (the_Edges_of G) \ (cv .edgesInOut() ) by GLIB_000:50;
A11: (G2 .order() ) + 1 = k by A2, GLIB_000:51;

A12: now

let C be Component of G2; :: thesis:

now

consider x being Vertex of C;
assume A13: for a being Vertex of C
for e being set holds not e Joins cv,a,G ; :: thesis:
the_Vertices_of C c= the_Vertices_of G2 ;
then reconsider x9 = x as Vertex of G2 by TARSKI:def 3;
the_Vertices_of G2 c= the_Vertices_of G ;
then reconsider x99 = x9 as Vertex of G by TARSKI:def 3;
consider W being Walk of G such that
A14: W is_Walk_from cv,x99 by Def1;
consider P being Path of W;
A15: P is_Walk_from cv,x99 by A14, GLIB_001:161;
then A16: P .first() = cv by GLIB_001:def 23;
set P2 = P .cut ((2 * 1) + 1),(len P);
A17: 1 <= len P by ABIAN:12;
A18: P .last() = x by A15, GLIB_001:def 23;
then A19: P . (len P) = x by GLIB_001:def 7;
not x9 in {cv} by A9, XBOOLE_0:def 5;
then A20: x <> cv by TARSKI:def 1;
then A21: not P is trivial by A16, A18, GLIB_001:128;
then A22: (2 * 1) + 1 <= len P by GLIB_001:126;
then P .cut ((2 * 1) + 1),(len P) is_Walk_from P . 3,P . (len P) by GLIB_001:38;
then A23: P .cut ((2 * 1) + 1),(len P) is_Walk_from P . 3,x by A18, GLIB_001:def 7;
A24: P . ((2 * 0 ) + 1) = cv by A16, GLIB_001:def 6;

now

assume cv in (P .cut ((2 * 1) + 1),(len P)) .vertices() ; :: thesis:
then consider n being odd Element of NAT such that
A25: n <= len (P .cut ((2 * 1) + 1),(len P)) and
A26: (P .cut ((2 * 1) + 1),(len P)) . n = cv by GLIB_001:88;
A27: 1 <= n by ABIAN:12;
then A28: 1 + 0 < n + 2 by XREAL_1:10;
A29: n in dom (P .cut ((2 * 1) + 1),(len P)) by A25, A27, FINSEQ_3:27;
then (3 + n) - 1 in dom P by A22, GLIB_001:48;
then A30: 2 + n <= len P by FINSEQ_3:27;
P . ((3 + n) - 1) = cv by A22, A26, A29, GLIB_001:48;
hence contradiction by A20, A24, A19, A30, A28, GLIB_001:def 28; :: thesis:

end;

then reconsider P2 = P .cut ((2 * 1) + 1),(len P) as Walk of G2 by GLIB_001:172;
P2 is_Walk_from P . 3,x by A23, GLIB_001:20;
then P2 .reverse() is_Walk_from x,P . 3 by GLIB_001:24;
then A31: P . 3 in G2 .reachableFrom x9 by Def5;
len P <> 1 by A21, GLIB_001:126;
then (2 * 0 ) + 1 < len P by A17, XXREAL_0:1;
then P . (1 + 1) Joins P . 1,P . (1 + 2),G by GLIB_001:def 3;
then A32: P . 2 Joins cv,P . 3,G by A16, GLIB_001:def 6;
the_Vertices_of C = G2 .reachableFrom x9 by Lm16;
hence contradiction by A13, A32, A31; :: thesis:

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 15;

now

per cases ;

suppose C is trivial ; :: thesis:

then consider v99 being Vertex of C such that
A35: the_Vertices_of C = {v99} by GLIB_000:25;
the_Vertices_of C c= the_Vertices_of G2 ;
then reconsider v9 = v99 as Vertex of G2 by TARSKI:def 3;
reconsider v = v9 as Vertex of G by GLIB_000:45;
take v = v; :: thesis:
thus v in the_Vertices_of C ; :: thesis:
not v9 in {cv} by A9, XBOOLE_0:def 5;
then A36: v9 <> cv by TARSKI:def 1;
A37: {v9} = G2 .reachableFrom v9 by A35, Lm16;

now

consider G3 being removeVertex of G,v;

A38: now

let e, z be set ; :: thesis:
assume A39: e Joins v,z,G ; :: thesis:
then A40: e in the_Edges_of G by GLIB_000:def 15;

now

assume that
A41: z <> v and
A42: z <> cv ; :: thesis:
not e in cv .edgesInOut() by A36, A39, A42, GLIB_000:68;
then e in the_Edges_of G2 by A10, A40, XBOOLE_0:def 5;
then e Joins v,z,G2 by A39, GLIB_000:76;
then z in G2 .reachableFrom v9 by Lm1, Lm2;
hence contradiction by A37, A41, TARSKI:def 1; :: thesis:

end;

hence ( z = v or z = cv ) ; :: thesis:

end;

now

let x, y be Vertex of G3; :: thesis:

now

per cases ;

suppose A43: x = y ; :: thesis:

set W = G3 .walkOf x;
take W = G3 .walkOf x; :: thesis:
thus W is_Walk_from x,y by A43, GLIB_001:14; :: thesis:

end;

suppose A44: x <> y ; :: thesis:

reconsider x9 = x, y9 = y as Vertex of G by GLIB_000:45;
consider W being Walk of G such that
A45: W is_Walk_from x9,y9 by Def1;
consider P being Path of W;
A46: P is_Walk_from x9,y9 by A45, GLIB_001:161;
A47: the_Vertices_of G3 = (the_Vertices_of G) \ {v} by GLIB_000:50;
then not x in {v} by XBOOLE_0:def 5;
then x <> v by TARSKI:def 1;
then A48: v <> P . 1 by A46, GLIB_001:18;
not y in {v} by A47, XBOOLE_0:def 5;
then y <> v by TARSKI:def 1;
then A49: v <> P . (len P) by A46, GLIB_001:18;

now

assume v in P .vertices() ; :: thesis:
then consider n being odd Element of NAT such that
A50: n <= len P and
A51: P . n = v by GLIB_001:88;
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:18;

A52: now

A53: n2 < n - 0 by XREAL_1:17;
assume P . n2 = v ; :: thesis:
hence contradiction by A48, A50, A51, A53, GLIB_001:def 28; :: thesis:

end;

set e1 = P . (n2 + 1);
set e2 = P . (n + 1);
n - 2 < (len P) - 0 by A50, XREAL_1:17;
then P . (n2 + 1) Joins P . n2,P . (n2 + 2),G by GLIB_001:def 3;
then A54: P . n2 = cv by A38, A51, A52, GLIB_000:17;
A55: n < len P by A49, A50, A51, XXREAL_0:1;
then A56: n + 2 <= len P by GLIB_001:1;

A57: now

A58: n + 0 < n + 2 by XREAL_1:10;
assume P . (n + 2) = v ; :: thesis:
hence contradiction by A48, A51, A56, A58, GLIB_001:def 28; :: thesis:

end;

n2 < n - 0 by XREAL_1:17;
then A59: n2 + 0 < n + 2 by XREAL_1:10;
P . (n + 1) Joins v,P . (n + 2),G by A51, A55, GLIB_001:def 3;
then A60: P . (n + 2) = cv by A38, A57;
then cv = P . 1 by A54, A56, A59, GLIB_001:def 28;
then A61: cv = x by A46, GLIB_001:18;
cv = P . (len P) by A54, A56, A60, A59, GLIB_001:def 28;
hence contradiction by A44, A46, A61, GLIB_001:18; :: thesis:

end;

then reconsider P = P as Walk of G3 by GLIB_001:172;
take P = P; :: thesis:
thus P is_Walk_from x,y by A46, GLIB_001:20; :: thesis:

end;

hence ex P being Walk of G3 st P is_Walk_from x,y ; :: thesis:

end;

then A62: G3 is connected by Def1;
assume v is cut-vertex ; :: thesis:
then 1 < G3 .numComponents() by A3, Def11;
hence contradiction by A62, Lm18; :: thesis:

end;

hence not v is cut-vertex ; :: thesis:

end;

suppose not C is trivial ; :: thesis:

then reconsider C9 = C as non trivial _Graph ;
(C .order() ) + 0 < (G2 .order() ) + 1 by GLIB_000:78, XREAL_1:10;
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;
consider C9R1 being removeVertex of C9,v1;
A66: C9R1 is connected by A64, Lm20;
consider C9R2 being removeVertex of C9,v2;
A67: the_Vertices_of C9R1 = (the_Vertices_of C9) \ {v1} by GLIB_000:50;
v2 in the_Vertices_of G2 by GLIB_000:45;
then not v2 in {cv} by A9, XBOOLE_0:def 5;
then A68: v2 <> cv by TARSKI:def 1;
A69: the_Vertices_of C9R2 = (the_Vertices_of C9) \ {v2} by GLIB_000:50;
v1 in the_Vertices_of G2 by GLIB_000:45;
then not v1 in {cv} by A9, XBOOLE_0:def 5;
then A70: v1 <> cv by TARSKI:def 1;
A71: C9R2 is connected by A65, Lm20;

now

per cases ;

suppose A72: not v1 in cv .allNeighbors() ; :: thesis:

reconsider v9 = v1 as Vertex of G2 by GLIB_000:45;
reconsider v = v9 as Vertex of G by GLIB_000:45;
take v = v; :: thesis:
thus v in the_Vertices_of C ; :: thesis:
consider G3 being removeVertex of G,v;
A73: the_Vertices_of G3 = (the_Vertices_of G) \ {v} by GLIB_000:50;
not cv in {v} by A70, TARSKI:def 1;
then reconsider cv9 = cv as Vertex of G3 by A73, XBOOLE_0:def 5;
A74: v1 <> a by A33, A72, GLIB_000:74;
A75: the_Vertices_of C = G2 .reachableFrom v9 by Lm16;

now

let y be Vertex of G3; :: thesis:

now

per cases ;

suppose y = cv ; :: thesis:

then G3 .walkOf y is_Walk_from cv9,y by GLIB_001:14;
hence ex W being Walk of G3 st W is_Walk_from cv9,y ; :: thesis:

end;

suppose A76: y <> cv ; :: thesis:

now

per cases ;

suppose A77: y in the_Vertices_of C ; :: thesis:

not a in {v1} by A74, TARSKI:def 1;
then A78: a in the_Vertices_of C9R1 by A67, XBOOLE_0:def 5;
not y in {v1} by A73, XBOOLE_0:def 5;
then y in the_Vertices_of C9R1 by A67, A77, XBOOLE_0:def 5;
then consider W being Walk of C9R1 such that
A79: W is_Walk_from y,a by A66, A78, Def1;
A80: ( W . 1 = y & W . (len W) = a ) by A79, GLIB_001:18;

A81: now

assume v in W .vertices() ; :: thesis:
then not v in {v1} by A67, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis:

end;

not e in v .edgesInOut() by A33, A70, A74, GLIB_000:68;
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 42;
then e in G .edgesBetween ((the_Vertices_of G) \ {v}) by GLIB_000:38;
then e in the_Edges_of G3 by GLIB_000:50;
then e Joins cv,a,G3 by A33, GLIB_000:76;
then A82: e Joins a,cv,G3 by GLIB_000:17;
reconsider W = W as Walk of C by GLIB_001:168;
reconsider W = W as Walk of G2 by GLIB_001:168;
reconsider W = W as Walk of G by GLIB_001:168;
not v in W .vertices() by A81, GLIB_001:99;
then reconsider W = W as Walk of G3 by GLIB_001:172;
W is_Walk_from y,a by A80, GLIB_001:18;
then W .addEdge e is_Walk_from y,cv by A82, GLIB_001:67;
then (W .addEdge e) .reverse() is_Walk_from cv,y by GLIB_001:24;
hence ex W being Walk of G3 st W is_Walk_from cv9,y ; :: thesis:

end;

suppose A83: not y in the_Vertices_of C ; :: thesis:

reconsider y9 = y as Vertex of G by GLIB_000:45;
consider W being Walk of G such that
A84: W is_Walk_from cv,y9 by Def1;
consider P being Path of W;
A85: P is_Walk_from cv,y9 by A84, GLIB_001:161;
then A86: P . (len P) = y9 by GLIB_001:18;
A87: P . 1 = cv by A85, GLIB_001:18;

now

assume v in P .vertices() ; :: thesis:
then consider n being odd Element of NAT such that
A88: n <= len P and
A89: P . n = v by GLIB_001:88;
set P2 = P .cut n,(len P);
A90: P .cut n,(len P) is_Walk_from v,y9 by A86, A88, A89, GLIB_001:38;
1 <= n by ABIAN:12;
then A91: 1 < n by A70, A87, A89, XXREAL_0:1;

now

assume cv in (P .cut n,(len P)) .vertices() ; :: thesis:
then consider m being odd Element of NAT such that
A92: m <= len (P .cut n,(len P)) and
A93: (P .cut n,(len P)) . m = cv by GLIB_001:88;
1 <= m by ABIAN:12;
then A94: m in dom (P .cut n,(len P)) by A92, FINSEQ_3:27;
then A95: P . ((n + m) - 1) = cv by A88, A93, GLIB_001:48;
1 + 1 < n + m by A91, ABIAN:12, XREAL_1:10;
then (1 + 1) - 1 < (n + m) - 1 by XREAL_1:16;
then A96: (2 * 0 ) + 1 < (n + m) - 1 ;
A97: (n + m) - 1 in dom P by A88, A94, GLIB_001:48;
then (n + m) - 1 <= len P by FINSEQ_3:27;
hence contradiction by A76, A87, A86, A95, A97, A96, GLIB_001:def 28; :: thesis:

end;

then reconsider P2 = P .cut n,(len P) as Walk of G2 by GLIB_001:172;
P2 is_Walk_from v,y9 by A90, GLIB_001:20;
hence contradiction by A75, A83, Def5; :: thesis:

end;

then reconsider P = P as Walk of G3 by GLIB_001:172;
take P = P; :: thesis:
thus P is_Walk_from cv9,y by A85, GLIB_001:20; :: thesis:

end;

hence ex W being Walk of G3 st W is_Walk_from cv9,y ; :: thesis:

end;

hence ex W being Walk of G3 st W is_Walk_from cv9,y ; :: thesis:

end;

then G3 is connected by Lm6;
then G3 .numComponents() = 1 by Lm18;
hence not v is cut-vertex by A3, Def11; :: thesis:

end;

suppose A98: ( v1 in cv .allNeighbors() & not v2 in cv .allNeighbors() ) ; :: thesis:

reconsider v9 = v2 as Vertex of G2 by GLIB_000:45;
reconsider v = v9 as Vertex of G by GLIB_000:45;
take v = v; :: thesis:
thus v in the_Vertices_of C ; :: thesis:
consider G3 being removeVertex of G,v;
A99: the_Vertices_of G3 = (the_Vertices_of G) \ {v} by GLIB_000:50;
not cv in {v} by A68, TARSKI:def 1;
then reconsider cv9 = cv as Vertex of G3 by A99, XBOOLE_0:def 5;
A100: v2 <> a by A33, A98, GLIB_000:74;
A101: the_Vertices_of C = G2 .reachableFrom v9 by Lm16;

now

let y be Vertex of G3; :: thesis:

now

per cases ;

suppose y = cv ; :: thesis:

then G3 .walkOf y is_Walk_from cv9,y by GLIB_001:14;
hence ex W being Walk of G3 st W is_Walk_from cv9,y ; :: thesis:

end;

suppose A102: y <> cv ; :: thesis:

now

per cases ;

suppose A103: y in the_Vertices_of C ; :: thesis:

not a in {v2} by A100, TARSKI:def 1;
then A104: a in the_Vertices_of C9R2 by A69, XBOOLE_0:def 5;
not y in {v2} by A99, XBOOLE_0:def 5;
then y in the_Vertices_of C9R2 by A69, A103, XBOOLE_0:def 5;
then consider W being Walk of C9R2 such that
A105: W is_Walk_from y,a by A71, A104, Def1;
A106: ( W . 1 = y & W . (len W) = a ) by A105, GLIB_001:18;

A107: now

assume v in W .vertices() ; :: thesis:
then not v in {v2} by A69, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis:

end;

not e in v .edgesInOut() by A33, A68, A100, GLIB_000:68;
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 42;
then e in G .edgesBetween ((the_Vertices_of G) \ {v}) by GLIB_000:38;
then e in the_Edges_of G3 by GLIB_000:50;
then e Joins cv,a,G3 by A33, GLIB_000:76;
then A108: e Joins a,cv,G3 by GLIB_000:17;
reconsider W = W as Walk of C by GLIB_001:168;
reconsider W = W as Walk of G2 by GLIB_001:168;
reconsider W = W as Walk of G by GLIB_001:168;
not v in W .vertices() by A107, GLIB_001:99;
then reconsider W = W as Walk of G3 by GLIB_001:172;
W is_Walk_from y,a by A106, GLIB_001:18;
then W .addEdge e is_Walk_from y,cv by A108, GLIB_001:67;
then (W .addEdge e) .reverse() is_Walk_from cv,y by GLIB_001:24;
hence ex W being Walk of G3 st W is_Walk_from cv9,y ; :: thesis:

end;

suppose A109: not y in the_Vertices_of C ; :: thesis:

reconsider y9 = y as Vertex of G by GLIB_000:45;
consider W being Walk of G such that
A110: W is_Walk_from cv,y9 by Def1;
consider P being Path of W;
A111: P is_Walk_from cv,y9 by A110, GLIB_001:161;
then A112: P . (len P) = y9 by GLIB_001:18;
A113: P . 1 = cv by A111, GLIB_001:18;

now

assume v in P .vertices() ; :: thesis:
then consider n being odd Element of NAT such that
A114: n <= len P and
A115: P . n = v by GLIB_001:88;
set P2 = P .cut n,(len P);
A116: P .cut n,(len P) is_Walk_from v,y9 by A112, A114, A115, GLIB_001:38;
1 <= n by ABIAN:12;
then A117: 1 < n by A68, A113, A115, XXREAL_0:1;

now

assume cv in (P .cut n,(len P)) .vertices() ; :: thesis:
then consider m being odd Element of NAT such that
A118: m <= len (P .cut n,(len P)) and
A119: (P .cut n,(len P)) . m = cv by GLIB_001:88;
1 <= m by ABIAN:12;
then A120: m in dom (P .cut n,(len P)) by A118, FINSEQ_3:27;
then A121: P . ((n + m) - 1) = cv by A114, A119, GLIB_001:48;
1 + 1 < n + m by A117, ABIAN:12, XREAL_1:10;
then (1 + 1) - 1 < (n + m) - 1 by XREAL_1:16;
then A122: (2 * 0 ) + 1 < (n + m) - 1 ;
A123: (n + m) - 1 in dom P by A114, A120, GLIB_001:48;
then (n + m) - 1 <= len P by FINSEQ_3:27;
hence contradiction by A102, A113, A112, A121, A123, A122, GLIB_001:def 28; :: thesis:

end;

then reconsider P2 = P .cut n,(len P) as Walk of G2 by GLIB_001:172;
P2 is_Walk_from v,y9 by A116, GLIB_001:20;
hence contradiction by A101, A109, Def5; :: thesis:

end;

then reconsider P = P as Walk of G3 by GLIB_001:172;
take P = P; :: thesis:
thus P is_Walk_from cv9,y by A111, GLIB_001:20; :: thesis:

end;

hence ex W being Walk of G3 st W is_Walk_from cv9,y ; :: thesis:

end;

hence ex W being Walk of G3 st W is_Walk_from cv9,y ; :: thesis:

end;

then G3 is connected by Lm6;
then G3 .numComponents() = 1 by Lm18;
hence not v is cut-vertex by A3, Def11; :: thesis:

end;

suppose ( v1 in cv .allNeighbors() & v2 in cv .allNeighbors() ) ; :: thesis:

then consider e being set such that
A124: e Joins cv,v2,G by GLIB_000:74;
reconsider v9 = v1 as Vertex of G2 by GLIB_000:45;
set a = v2;
reconsider v = v9 as Vertex of G by GLIB_000:45;
take v = v; :: thesis:
thus v in the_Vertices_of C ; :: thesis:
consider G3 being removeVertex of G,v;
A125: the_Vertices_of G3 = (the_Vertices_of G) \ {v} by GLIB_000:50;
not cv in {v} by A70, TARSKI:def 1;
then reconsider cv9 = cv as Vertex of G3 by A125, XBOOLE_0:def 5;
A126: the_Vertices_of C = G2 .reachableFrom v9 by Lm16;
A127: e in the_Edges_of G by A124, GLIB_000:def 15;

now

let y be Vertex of G3; :: thesis:

now

per cases ;

suppose y = cv ; :: thesis:

then G3 .walkOf y is_Walk_from cv9,y by GLIB_001:14;
hence ex W being Walk of G3 st W is_Walk_from cv9,y ; :: thesis:

end;

suppose A128: y <> cv ; :: thesis:

now

per cases ;

suppose A129: y in the_Vertices_of C ; :: thesis:

not v2 in {v1} by A63, TARSKI:def 1;
then A130: v2 in the_Vertices_of C9R1 by A67, XBOOLE_0:def 5;
not y in {v1} by A125, XBOOLE_0:def 5;
then y in the_Vertices_of C9R1 by A67, A129, XBOOLE_0:def 5;
then consider W being Walk of C9R1 such that
A131: W is_Walk_from y,v2 by A66, A130, Def1;
A132: ( W . 1 = y & W . (len W) = v2 ) by A131, GLIB_001:18;

A133: now

assume v in W .vertices() ; :: thesis:
then not v in {v1} by A67, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis:

end;

not e in v .edgesInOut() by A63, A70, A124, GLIB_000:68;
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 42;
then e in G .edgesBetween ((the_Vertices_of G) \ {v}) by GLIB_000:38;
then e in the_Edges_of G3 by GLIB_000:50;
then e Joins cv,v2,G3 by A124, GLIB_000:76;
then A134: e Joins v2,cv,G3 by GLIB_000:17;
reconsider W = W as Walk of C by GLIB_001:168;
reconsider W = W as Walk of G2 by GLIB_001:168;
reconsider W = W as Walk of G by GLIB_001:168;
not v in W .vertices() by A133, GLIB_001:99;
then reconsider W = W as Walk of G3 by GLIB_001:172;
W is_Walk_from y,v2 by A132, GLIB_001:18;
then W .addEdge e is_Walk_from y,cv by A134, GLIB_001:67;
then (W .addEdge e) .reverse() is_Walk_from cv,y by GLIB_001:24;
hence ex W being Walk of G3 st W is_Walk_from cv9,y ; :: thesis:

end;

suppose A135: not y in the_Vertices_of C ; :: thesis:

reconsider y9 = y as Vertex of G by GLIB_000:45;
consider W being Walk of G such that
A136: W is_Walk_from cv,y9 by Def1;
consider P being Path of W;
A137: P is_Walk_from cv,y9 by A136, GLIB_001:161;
then A138: P . (len P) = y9 by GLIB_001:18;
A139: P . 1 = cv by A137, GLIB_001:18;

now

assume v in P .vertices() ; :: thesis:
then consider n being odd Element of NAT such that
A140: n <= len P and
A141: P . n = v by GLIB_001:88;
set P2 = P .cut n,(len P);
A142: P .cut n,(len P) is_Walk_from v,y9 by A138, A140, A141, GLIB_001:38;
1 <= n by ABIAN:12;
then A143: 1 < n by A70, A139, A141, XXREAL_0:1;

now

assume cv in (P .cut n,(len P)) .vertices() ; :: thesis:
then consider m being odd Element of NAT such that
A144: m <= len (P .cut n,(len P)) and
A145: (P .cut n,(len P)) . m = cv by GLIB_001:88;
1 <= m by ABIAN:12;
then A146: m in dom (P .cut n,(len P)) by A144, FINSEQ_3:27;
then A147: P . ((n + m) - 1) = cv by A140, A145, GLIB_001:48;
1 + 1 < n + m by A143, ABIAN:12, XREAL_1:10;
then (1 + 1) - 1 < (n + m) - 1 by XREAL_1:16;
then A148: (2 * 0 ) + 1 < (n + m) - 1 ;
A149: (n + m) - 1 in dom P by A140, A146, GLIB_001:48;
then (n + m) - 1 <= len P by FINSEQ_3:27;
hence contradiction by A128, A139, A138, A147, A149, A148, GLIB_001:def 28; :: thesis:

end;

then reconsider P2 = P .cut n,(len P) as Walk of G2 by GLIB_001:172;
P2 is_Walk_from v,y9 by A142, GLIB_001:20;
hence contradiction by A126, A135, Def5; :: thesis:

end;

then reconsider P = P as Walk of G3 by GLIB_001:172;
take P = P; :: thesis:
thus P is_Walk_from cv9,y by A137, GLIB_001:20; :: thesis:

end;

hence ex W being Walk of G3 st W is_Walk_from cv9,y ; :: thesis:

end;

hence ex W being Walk of G3 st W is_Walk_from cv9,y ; :: thesis:

end;

then G3 is connected by Lm6;
then G3 .numComponents() = 1 by Lm18;
hence not v is cut-vertex by A3, Def11; :: thesis:

end;

hence ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex ) ; :: thesis:

end;

hence ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex ) ; :: thesis:

end;

then consider v1 being Vertex of G such that
A150: v1 in the_Vertices_of CC1 and
A151: not v1 is cut-vertex ;
consider v2 being Vertex of G such that
A152: v2 in the_Vertices_of CC2 and
A153: not v2 is cut-vertex by A12;
take v1 = v1; :: thesis:
take v2 = v2; :: thesis:

now

C2 is non empty Subset of (the_Vertices_of G2) by Lm13;
then A154: the_Vertices_of CC2 = C2 by GLIB_000:def 39;
C1 is non empty Subset of (the_Vertices_of G2) by Lm13;
then A155: the_Vertices_of CC1 = C1 by GLIB_000:def 39;
assume v1 = v2 ; :: thesis:
then CC1 == CC2 by A150, A152, Lm17;
hence contradiction by A8, A155, A154, GLIB_000:def 36; :: thesis:

end;

hence v1 <> v2 ; :: thesis:
thus ( not v1 is cut-vertex & not v2 is cut-vertex ) by A151, A153; :: thesis:

end;

hence ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex ) ; :: thesis:

end;

hence S₁[k] ; :: thesis:

end;

then A156: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k] ;
A157: for k being Nat holds S₁[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; :: thesis: