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