:: deftheorem defines Degree GRAPH_1:def 23 :
for G being finite Graph
for x being Vertex of G holds Degree x = (EdgesIn x) + (EdgesOut x);