theorem Th48: :: GRAPH_3:48

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 & v <> v1 & v <> v2 holds
Degree (v9,X) = Degree (v,X)