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