:: deftheorem Def8 defines degree SGRAPH1:def 8 :
for X being set
for G being SimpleGraph of X
for v being set
for b₄ being Element of NAT holds
( b₄ = degree (G,v) iff ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & b₄ = card X ) );