theorem :: GLIBPRE0:49

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