theorem Th23: :: GRAPH_3:23

for G being finite Graph
for v being Vertex of G holds card (Edges_Out v) = EdgesOut v