theorem Th45: :: GLIBPRE1:44

for G being loopless complete _Graph
for v being Vertex of G holds v .allNeighbors() = (the_Vertices_of G) \ {v}