theorem Th31: :: GRAPH_3:31

for X being set
for G being finite Graph
for v being Vertex of G holds Degree (v,X) = Degree (v,(X /\ the carrier' of G))