theorem Th11: :: GLIB_016:11

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