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