theorem Th47: :: GRAPH_3:47

for X being set
for G being finite Graph
for v, v1, v2 being Vertex of G
for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v & v1 <> v2 & ( v = v1 or v = v2 ) & the carrier' of G in X holds
Degree (v9,X) = (Degree (v,X)) + 1