:: deftheorem defines Degree GRAPH_3:def 6 :
for G being finite Graph
for v being Vertex of G
for X being set holds Degree (v,X) = (card (Edges_In (v,X))) + (card (Edges_Out (v,X)));