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