let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V
for v being Vertex of G1 st v in V \ (the_Vertices_of G2) holds
( v is isolated & not v is cut-vertex )
let V be set ; :: thesis: for G1 being addVertices of G2,V
for v being Vertex of G1 st v in V \ (the_Vertices_of G2) holds
( v is isolated & not v is cut-vertex )
let G1 be addVertices of G2,V; :: thesis: for v being Vertex of G1 st v in V \ (the_Vertices_of G2) holds
( v is isolated & not v is cut-vertex )
let v be Vertex of G1; :: thesis: ( v in V \ (the_Vertices_of G2) implies ( v is isolated & not v is cut-vertex ) )
assume A1: v in V \ (the_Vertices_of G2) ; :: thesis: ( v is isolated & not v is cut-vertex )
v .edgesInOut() = {}

proof

assume v .edgesInOut() <> {} ; :: thesis: contradiction
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 ( (the_Source_of G1) . e = v or (the_Target_of G1) . e = v ) by A2, GLIB_000:61;

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

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: verum

end;

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

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: verum

end;

end;

end;

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