theorem Th12: :: GLIB_016:12

for G being loopless Dcomplete _Graph
for v being Vertex of G holds
( v .inNeighbors() = (the_Vertices_of G) \ {v} & v .outNeighbors() = (the_Vertices_of G) \ {v} & v .allNeighbors() = (the_Vertices_of G) \ {v} )