let G be loopless Dcomplete _Graph; :: thesis: 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} )
let v be Vertex of G; :: thesis: ( v .inNeighbors() = (the_Vertices_of G) \ {v} & v .outNeighbors() = (the_Vertices_of G) \ {v} & v .allNeighbors() = (the_Vertices_of G) \ {v} )
A1: ( (the_Vertices_of G) \ {v} c= v .inNeighbors() & (the_Vertices_of G) \ {v} c= v .outNeighbors() & (the_Vertices_of G) \ {v} c= v .allNeighbors() ) by Th11;
A2: ( v .inNeighbors() c= (the_Vertices_of G) \ {v} & v .outNeighbors() c= (the_Vertices_of G) \ {v} & v .allNeighbors() c= (the_Vertices_of G) \ {v} ) by GLIB_000:175;
thus v .inNeighbors() = (the_Vertices_of G) \ {v} by A1, A2, XBOOLE_0:def 10; :: thesis: ( v .outNeighbors() = (the_Vertices_of G) \ {v} & v .allNeighbors() = (the_Vertices_of G) \ {v} )
thus v .outNeighbors() = (the_Vertices_of G) \ {v} by A1, A2, XBOOLE_0:def 10; :: thesis: v .allNeighbors() = (the_Vertices_of G) \ {v}
thus v .allNeighbors() = (the_Vertices_of G) \ {v} by A1, A2, XBOOLE_0:def 10; :: thesis: verum