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 ;
then A5: not G2 is trivial by ;
let G2A be removeVertex of G2,v2; :: according to GLIB_002:def 10 :: thesis:
set G1A = the removeVertex of G1,v1;
G1 .numComponents() = G2 .numComponents() by ;
then A6: G2 .numComponents() in the removeVertex of G1,v1 .numComponents() by A3;
the_Vertices_of the removeVertex of G1,v1 = () \ {v2} by
.= () \ {v2} by ;
then A7: the_Vertices_of G2A = the_Vertices_of the removeVertex of G1,v1 by ;
G2 is Subgraph of G1 by ;
then A8: G2A is Subgraph of G1 by GLIB_000:43;
the_Edges_of the removeVertex of G1,v1 = G1 .edgesBetween (() \ {v1}) by
.= G1 .edgesBetween (() \ {v2}) by
.= G2 .edgesBetween (() \ {v2}) by ;
then the_Edges_of G2A = the_Edges_of the removeVertex of G1,v1 by ;
hence G2 .numComponents() in G2A .numComponents() by ; :: thesis: verum