for X being non empty set
for g being SimpleGraph of X
for v being set st v in the carrier of g holds
ex VV being finite set st
( VV = the carrier of g & degree (g,v) < card VV )