for G being simple complete _Graph
for v being Vertex of G holds (v .degree()) +` 1 = G .order()