theorem Th22: :: GRAPH_3:22

for G being finite Graph
for v being Vertex of G holds card (Edges_In v) = EdgesIn v