theorem :: GLIB_000:175

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