let G2 be _Graph; :: thesis:
let V be set ; :: thesis:
let G1 be addVertices of G2,V; :: thesis:
let v be Vertex of G1; :: thesis:
assume A1: v in V \ (the_Vertices_of G2) ; :: thesis:
v .edgesInOut() = {}

assume v .edgesInOut() <> {} ; :: thesis:
then consider e being object such that
A2: e in v .edgesInOut() by XBOOLE_0:def 1;
e in the_Edges_of G1 by A2;
then A3: e in the_Edges_of G2 by Def10;

per cases ) . e = v or (the_Target_of G1) . e = v ) by A2, GLIB_000:61;

suppose (the_Source_of G1) . e = v ; :: thesis:

then (the_Source_of G2) . e = v by Def10;
then v in the_Vertices_of G2 by A3, FUNCT_2:5;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis:

end;

suppose (the_Target_of G1) . e = v ; :: thesis:

then (the_Target_of G2) . e = v by Def10;
then v in the_Vertices_of G2 by A3, FUNCT_2:5;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis:

end;

end;

end;

hence v is isolated by GLIB_000:def 49; :: thesis:
hence not v is cut-vertex ; :: thesis: