theorem Th28: :: SGRAPH1:28

for X being non empty set
for G being SimpleGraph of X
for v being set ex ww being finite set st
( ww = { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } & degree (G,v) = card ww )