theorem Th11: :: GLPACY00:7

for G2 being _Graph
for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for w1 being Vertex of G1 st not e in the_Edges_of G2 & not v in the_Vertices_of G2 & w1 = w holds
( w1 .edgesIn() = (w .edgesIn()) \/ {e} & w1 .inDegree() = (w .inDegree()) +` 1 & w1 .edgesOut() = w .edgesOut() & w1 .outDegree() = w .outDegree() & w1 .edgesInOut() = (w .edgesInOut()) \/ {e} & w1 .degree() = (w .degree()) +` 1 )