let G1, G2 be _Graph; :: thesis: for v1 being Vertex of G1

for v2 being Vertex of G2 st G1 == G2 & v1 = v2 & v1 is cut-vertex holds

v2 is cut-vertex

let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st G1 == G2 & v1 = v2 & v1 is cut-vertex holds

v2 is cut-vertex

let v2 be Vertex of G2; :: thesis: ( G1 == G2 & v1 = v2 & v1 is cut-vertex implies v2 is cut-vertex )

assume that

A1: G1 == G2 and

A2: v1 = v2 and

A3: v1 is cut-vertex ; :: thesis: v2 is cut-vertex

A4: not G1 is _trivial by A3, Th37;

then A5: not G2 is _trivial by A1, GLIB_000:89;

let G2A be removeVertex of G2,v2; :: according to GLIB_002:def 10 :: thesis: G2 .numComponents() in G2A .numComponents()

set G1A = the removeVertex of G1,v1;

G1 .numComponents() = G2 .numComponents() by A1, Lm12;

then A6: G2 .numComponents() in the removeVertex of G1,v1 .numComponents() by A3;

the_Vertices_of the removeVertex of G1,v1 = (the_Vertices_of G1) \ {v2} by A2, A4, GLIB_000:47

.= (the_Vertices_of G2) \ {v2} by A1, GLIB_000:def 34 ;

then A7: the_Vertices_of G2A = the_Vertices_of the removeVertex of G1,v1 by A5, GLIB_000:47;

G2 is Subgraph of G1 by A1, GLIB_000:87;

then A8: G2A is Subgraph of G1 by GLIB_000:43;

the_Edges_of the removeVertex of G1,v1 = G1 .edgesBetween ((the_Vertices_of G1) \ {v1}) by A4, GLIB_000:47

.= G1 .edgesBetween ((the_Vertices_of G2) \ {v2}) by A1, A2, GLIB_000:def 34

.= G2 .edgesBetween ((the_Vertices_of G2) \ {v2}) by A1, GLIB_000:90 ;

then the_Edges_of G2A = the_Edges_of the removeVertex of G1,v1 by A5, GLIB_000:47;

hence G2 .numComponents() in G2A .numComponents() by A6, A7, A8, Lm12, GLIB_000:86; :: thesis: verum

for v2 being Vertex of G2 st G1 == G2 & v1 = v2 & v1 is cut-vertex holds

v2 is cut-vertex

let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st G1 == G2 & v1 = v2 & v1 is cut-vertex holds

v2 is cut-vertex

let v2 be Vertex of G2; :: thesis: ( G1 == G2 & v1 = v2 & v1 is cut-vertex implies v2 is cut-vertex )

assume that

A1: G1 == G2 and

A2: v1 = v2 and

A3: v1 is cut-vertex ; :: thesis: v2 is cut-vertex

A4: not G1 is _trivial by A3, Th37;

then A5: not G2 is _trivial by A1, GLIB_000:89;

let G2A be removeVertex of G2,v2; :: according to GLIB_002:def 10 :: thesis: G2 .numComponents() in G2A .numComponents()

set G1A = the removeVertex of G1,v1;

G1 .numComponents() = G2 .numComponents() by A1, Lm12;

then A6: G2 .numComponents() in the removeVertex of G1,v1 .numComponents() by A3;

the_Vertices_of the removeVertex of G1,v1 = (the_Vertices_of G1) \ {v2} by A2, A4, GLIB_000:47

.= (the_Vertices_of G2) \ {v2} by A1, GLIB_000:def 34 ;

then A7: the_Vertices_of G2A = the_Vertices_of the removeVertex of G1,v1 by A5, GLIB_000:47;

G2 is Subgraph of G1 by A1, GLIB_000:87;

then A8: G2A is Subgraph of G1 by GLIB_000:43;

the_Edges_of the removeVertex of G1,v1 = G1 .edgesBetween ((the_Vertices_of G1) \ {v1}) by A4, GLIB_000:47

.= G1 .edgesBetween ((the_Vertices_of G2) \ {v2}) by A1, A2, GLIB_000:def 34

.= G2 .edgesBetween ((the_Vertices_of G2) \ {v2}) by A1, GLIB_000:90 ;

then the_Edges_of G2A = the_Edges_of the removeVertex of G1,v1 by A5, GLIB_000:47;

hence G2 .numComponents() in G2A .numComponents() by A6, A7, A8, Lm12, GLIB_000:86; :: thesis: verum