theorem :: GLIB_000:176

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