theorem Th1: :: GLIB_016:1

for c being non empty Cardinal
for v being Vertex of (canCompleteGraph c) holds
( v .inNeighbors() = v & v .outNeighbors() = c \ (succ v) )