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 S_{1}[ 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 );

S_{1}[n] ) holds

S_{1}[k]
;

A157: for k being Nat holds S_{1}[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: verum

( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )

defpred S

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

S_{1}[n] ) holds

S_{1}[k]

then A156:
for k being Nat st ( for n being Nat st n < k holds S

S

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds

S_{1}[n] ) implies S_{1}[k] )

assume A1: for n being Nat st n < k holds

S_{1}[n]
; :: thesis: S_{1}[k]

_{1}[k]
; :: thesis: verum

end;S

assume A1: for n being Nat st n < k holds

S

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 )

hence
Sex 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;

( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex ) ; :: thesis: verum

end;( 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 )end;

hence
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 )
;

end;

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 )

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

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 )

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

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 )

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

end;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 :: 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 )

then consider v1 being Vertex of G such that ( 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 )

A33: e Joins cv,a,G ;

A34: e in the_Edges_of G by A33, GLIB_000:def 13;

( v in the_Vertices_of C & not v is cut-vertex ) ; :: thesis: verum

end;( 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

then consider a being Vertex of C, e being set such that 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 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: not 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;

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; :: thesis: verum

end;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 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: not 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 :: thesis: not cv in ( the Path of W .cut (((2 * 1) + 1),(len the Path of W))) .vertices()

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;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 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; :: thesis: verum

end;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 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; :: thesis: verum

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; :: thesis: verum

A33: e Joins cv,a,G ;

A34: e in the_Edges_of G by A33, GLIB_000:def 13;

now :: thesis: ex v being Vertex of G st

( v in the_Vertices_of C & not v is cut-vertex )end;

hence
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 )
;

end;

suppose
C is trivial
; :: thesis: ex v being Vertex of G st

( v in the_Vertices_of C & not v is cut-vertex )

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

end;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 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 :: thesis: not v is cut-vertex

hence
not v is cut-vertex
; :: thesis: verumset G3 = the removeVertex of G,v;

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;A38: now :: thesis: for e, z being set holds

( not e Joins v,z,G or z = v or z = cv )

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

end;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 )

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

A41: z <> v and

A42: z <> cv ; :: thesis: 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; :: thesis: verum

end;A41: z <> v and

A42: z <> cv ; :: thesis: 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; :: thesis: verum

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

then A62:
the removeVertex of G,v is connected
;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

end;now :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from x,yend;

hence
ex P being Walk of the removeVertex of G,v st P is_Walk_from x,y
; :: thesis: verumper cases
( x = y or x <> y )
;

end;

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 A43, GLIB_001:13; :: thesis: verum

end;take W = the removeVertex of G,v .walkOf x; :: thesis: W is_Walk_from x,y

thus W is_Walk_from x,y by A43, GLIB_001:13; :: thesis: verum

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

take P = P; :: thesis: P is_Walk_from x,y

thus P is_Walk_from x,y by A46, GLIB_001:19; :: thesis: verum

end;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 :: thesis: not v in the Path of W .vertices()

then reconsider P = the Path of W as Walk of the removeVertex of G,v by GLIB_001:171;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 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 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;

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; :: thesis: verum

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

A52: now :: thesis: not the Path of W . n2 = v

set e1 = the Path of W . (n2 + 1);A53:
n2 < n - 0
by XREAL_1:15;

assume the Path of W . n2 = v ; :: thesis: contradiction

hence contradiction by A48, A50, A51, A53, GLIB_001:def 28; :: thesis: verum

end;assume the Path of W . n2 = v ; :: thesis: contradiction

hence contradiction by A48, A50, A51, A53, GLIB_001:def 28; :: thesis: verum

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;

A57: now :: thesis: not the Path of W . (n + 2) = v

n2 < n - 0
by XREAL_1:15;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;assume the Path of W . (n + 2) = v ; :: thesis: contradiction

hence contradiction by A48, A51, A56, A58, GLIB_001:def 28; :: thesis: verum

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; :: thesis: verum

take P = P; :: thesis: P is_Walk_from x,y

thus P is_Walk_from x,y by A46, GLIB_001:19; :: thesis: verum

assume v is cut-vertex ; :: thesis: contradiction

then 1 < the removeVertex of G,v .numComponents() by A3;

hence contradiction by A62, Lm18; :: thesis: verum

suppose
not C is trivial
; :: thesis: ex v being Vertex of G st

( v in the_Vertices_of C & not v is cut-vertex )

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

( v in the_Vertices_of C & not v is cut-vertex ) ; :: thesis: verum

end;(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 :: thesis: ex v being Vertex of G st

( v in the_Vertices_of C & not v is cut-vertex )end;

hence
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() ) )
;

end;

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 )

( 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 = (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;

then the removeVertex of G,v .numComponents() = 1 by Lm18;

hence not v is cut-vertex by A3; :: thesis: verum

end;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 = (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 :: 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

then
the removeVertex of G,v is connected
by Lm6;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

end;now :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,yend;

hence
ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
; :: thesis: verumper cases
( y = cv or y <> cv )
;

end;

suppose
y = cv
; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y

then
the removeVertex of G,v .walkOf y is_Walk_from cv9,y
by GLIB_001:13;

hence ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; :: thesis: verum

end;hence ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; :: thesis: verum

suppose A76:
y <> cv
; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y

end;

now :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,yend;

hence
ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
; :: thesis: verumper cases
( y in the_Vertices_of C or not y in the_Vertices_of C )
;

end;

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

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 ; :: thesis: verum

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

A81: now :: thesis: not v in W .vertices()

not e in v .edgesInOut()
by A33, A70, A74, GLIB_000:65;assume
v in W .vertices()
; :: thesis: contradiction

then not v in {v1} by A67, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then not v in {v1} by A67, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

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 ; :: thesis: verum

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

take P = P; :: thesis: P is_Walk_from cv9,y

thus P is_Walk_from cv9,y by A85, GLIB_001:19; :: thesis: verum

end;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 :: thesis: not v in the Path of W .vertices()

then reconsider P = the Path of W as Walk of the removeVertex of G,v by GLIB_001:171;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 A86, A88, A89, GLIB_001:37;

1 <= n by ABIAN:12;

then A91: 1 < n by A70, A87, A89, XXREAL_0:1;

P2 is_Walk_from v,y9 by A90, GLIB_001:19;

hence contradiction by A75, A83, Def5; :: thesis: verum

end;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 A86, A88, A89, GLIB_001:37;

1 <= n by ABIAN:12;

then A91: 1 < n by A70, A87, A89, XXREAL_0:1;

now :: thesis: not cv in ( the Path of W .cut (n,(len the Path of W))) .vertices()

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;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 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; :: thesis: verum

end;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 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; :: thesis: verum

P2 is_Walk_from v,y9 by A90, GLIB_001:19;

hence contradiction by A75, A83, Def5; :: thesis: verum

take P = P; :: thesis: P is_Walk_from cv9,y

thus P is_Walk_from cv9,y by A85, GLIB_001:19; :: thesis: verum

then the removeVertex of G,v .numComponents() = 1 by Lm18;

hence not v is cut-vertex by A3; :: thesis: verum

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 )

( 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 = (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;

then the removeVertex of G,v .numComponents() = 1 by Lm18;

hence not v is cut-vertex by A3; :: thesis: verum

end;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 = (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 :: 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

then
the removeVertex of G,v is connected
by Lm6;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

end;now :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,yend;

hence
ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
; :: thesis: verumper cases
( y = cv or y <> cv )
;

end;

suppose
y = cv
; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y

then
the removeVertex of G,v .walkOf y is_Walk_from cv9,y
by GLIB_001:13;

hence ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; :: thesis: verum

end;hence ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; :: thesis: verum

suppose A102:
y <> cv
; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y

end;

now :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,yend;

hence
ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
; :: thesis: verumper cases
( y in the_Vertices_of C or not y in the_Vertices_of C )
;

end;

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

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 ; :: thesis: verum

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

A107: now :: thesis: not v in W .vertices()

not e in v .edgesInOut()
by A33, A68, A100, GLIB_000:65;assume
v in W .vertices()
; :: thesis: contradiction

then not v in {v2} by A69, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then not v in {v2} by A69, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

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 ; :: thesis: verum

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

take P = P; :: thesis: P is_Walk_from cv9,y

thus P is_Walk_from cv9,y by A111, GLIB_001:19; :: thesis: verum

end;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 :: thesis: not v in the Path of W .vertices()

then reconsider P = the Path of W as Walk of the removeVertex of G,v by GLIB_001:171;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 A112, A114, A115, GLIB_001:37;

1 <= n by ABIAN:12;

then A117: 1 < n by A68, A113, A115, XXREAL_0:1;

P2 is_Walk_from v,y9 by A116, GLIB_001:19;

hence contradiction by A101, A109, Def5; :: thesis: verum

end;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 A112, A114, A115, GLIB_001:37;

1 <= n by ABIAN:12;

then A117: 1 < n by A68, A113, A115, XXREAL_0:1;

now :: thesis: not cv in ( the Path of W .cut (n,(len the Path of W))) .vertices()

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;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 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; :: thesis: verum

end;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 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; :: thesis: verum

P2 is_Walk_from v,y9 by A116, GLIB_001:19;

hence contradiction by A101, A109, Def5; :: thesis: verum

take P = P; :: thesis: P is_Walk_from cv9,y

thus P is_Walk_from cv9,y by A111, GLIB_001:19; :: thesis: verum

then the removeVertex of G,v .numComponents() = 1 by Lm18;

hence not v is cut-vertex by A3; :: thesis: verum

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 )

( 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 = (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;

then the removeVertex of G,v .numComponents() = 1 by Lm18;

hence not v is cut-vertex by A3; :: thesis: verum

end;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 = (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 :: 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

then
the removeVertex of G,v is connected
by Lm6;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

end;now :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,yend;

hence
ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
; :: thesis: verumper cases
( y = cv or y <> cv )
;

end;

suppose
y = cv
; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y

then
the removeVertex of G,v .walkOf y is_Walk_from cv9,y
by GLIB_001:13;

hence ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; :: thesis: verum

end;hence ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; :: thesis: verum

suppose A128:
y <> cv
; :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y

end;

now :: thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,yend;

hence
ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
; :: thesis: verumper cases
( y in the_Vertices_of C or not y in the_Vertices_of C )
;

end;

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

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 ; :: thesis: verum

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

A133: now :: thesis: not v in W .vertices()

not e in v .edgesInOut()
by A63, A70, A124, GLIB_000:65;assume
v in W .vertices()
; :: thesis: contradiction

then not v in {v1} by A67, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then not v in {v1} by A67, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

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 ; :: thesis: verum

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

take P = P; :: thesis: P is_Walk_from cv9,y

thus P is_Walk_from cv9,y by A137, GLIB_001:19; :: thesis: verum

end;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 :: thesis: not v in the Path of W .vertices()

then reconsider P = the Path of W as Walk of the removeVertex of G,v by GLIB_001:171;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 A138, A140, A141, GLIB_001:37;

1 <= n by ABIAN:12;

then A143: 1 < n by A70, A139, A141, XXREAL_0:1;

P2 is_Walk_from v,y9 by A142, GLIB_001:19;

hence contradiction by A126, A135, Def5; :: thesis: verum

end;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 A138, A140, A141, GLIB_001:37;

1 <= n by ABIAN:12;

then A143: 1 < n by A70, A139, A141, XXREAL_0:1;

now :: thesis: not cv in ( the Path of W .cut (n,(len the Path of W))) .vertices()

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;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 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; :: thesis: verum

end;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 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; :: thesis: verum

P2 is_Walk_from v,y9 by A142, GLIB_001:19;

hence contradiction by A126, A135, Def5; :: thesis: verum

take P = P; :: thesis: P is_Walk_from cv9,y

thus P is_Walk_from cv9,y by A137, GLIB_001:19; :: thesis: verum

then the removeVertex of G,v .numComponents() = 1 by Lm18;

hence not v is cut-vertex by A3; :: thesis: verum

( v in the_Vertices_of C & not v is cut-vertex ) ; :: thesis: verum

( v in the_Vertices_of C & not v is cut-vertex ) ; :: thesis: verum

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 )

now :: thesis: not v1 = v2

hence
v1 <> v2
; :: thesis: ( not v1 is cut-vertex & not v2 is cut-vertex )
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 ; :: thesis: contradiction

then 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; :: thesis: verum

end;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 ; :: thesis: contradiction

then 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; :: thesis: verum

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

( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex ) ; :: thesis: verum

S

S

A157: for k being Nat holds S

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