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 A1: ( G1 == G2 & v1 = v2 & v1 is cut-vertex ) ; :: thesis: v2 is cut-vertex
then A2: G1 .numComponents() = G2 .numComponents() by Lm12;
consider G1A being removeVertex of G1,v1;
A3: G2 .numComponents() in G1A .numComponents() by A1, A2, Def10;
A4: not G1 is trivial by A1, Th38;
then A5: the_Vertices_of G1A = (the_Vertices_of G1) \ {v2} by A1, GLIB_000:50
.= (the_Vertices_of G2) \ {v2} by A1, GLIB_000:def 36 ;
A6: the_Edges_of G1A = G1 .edgesBetween ((the_Vertices_of G1) \ {v1}) by A4, GLIB_000:50
.= G1 .edgesBetween ((the_Vertices_of G2) \ {v2}) by A1, GLIB_000:def 36
.= G2 .edgesBetween ((the_Vertices_of G2) \ {v2}) by A1, GLIB_000:93 ;
let G2A be removeVertex of G2,v2; :: according to GLIB_002:def 10 :: thesis: G2 .numComponents() in G2A .numComponents()
A7: not G2 is trivial by A1, A4, GLIB_000:92;
then A8: the_Vertices_of G2A = the_Vertices_of G1A by A5, GLIB_000:50;
A9: the_Edges_of G2A = the_Edges_of G1A by A6, A7, GLIB_000:50;
G2 is Subgraph of G1 by A1, GLIB_000:90;
then G2A is Subgraph of G1 by GLIB_000:46;
hence G2 .numComponents() in G2A .numComponents() by A3, A8, A9, Lm12, GLIB_000:89; :: thesis: verum