let G be Dcomplete _Graph; :: thesis: 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() )
let v be Vertex of G; :: thesis: ( (the_Vertices_of G) \ {v} c= v .inNeighbors() & (the_Vertices_of G) \ {v} c= v .outNeighbors() & (the_Vertices_of G) \ {v} c= v .allNeighbors() )

A1: now :: thesis: for x being object st x in (the_Vertices_of G) \ {v} holds
( x in v .inNeighbors() & x in v .outNeighbors() & x in v .allNeighbors() )

let x be object ; :: thesis: ( x in (the_Vertices_of G) \ {v} implies ( x in v .inNeighbors() & x in v .outNeighbors() & x in v .allNeighbors() ) )
assume x in (the_Vertices_of G) \ {v} ; :: thesis: ( x in v .inNeighbors() & x in v .outNeighbors() & x in v .allNeighbors() )
then A2: ( x in the_Vertices_of G & x <> v ) by ZFMISC_1:56;
then reconsider w = x as Vertex of G ;
ex e being object st e DJoins w,v,G by A2, Def1;
hence x in v .inNeighbors() by GLIB_000:69; :: thesis: ( x in v .outNeighbors() & x in v .allNeighbors() )
consider e being object such that
A3: e DJoins v,w,G by A2, Def1;
thus x in v .outNeighbors() by A3, GLIB_000:70; :: thesis: x in v .allNeighbors()
e Joins v,w,G by A3, GLIB_000:16;
hence x in v .allNeighbors() by GLIB_000:71; :: thesis: verum

end;

then for x being object st x in (the_Vertices_of G) \ {v} holds
x in v .inNeighbors() ;
hence (the_Vertices_of G) \ {v} c= v .inNeighbors() by TARSKI:def 3; :: thesis: ( (the_Vertices_of G) \ {v} c= v .outNeighbors() & (the_Vertices_of G) \ {v} c= v .allNeighbors() )
for x being object st x in (the_Vertices_of G) \ {v} holds
x in v .outNeighbors() by A1;
hence (the_Vertices_of G) \ {v} c= v .outNeighbors() by TARSKI:def 3; :: thesis: (the_Vertices_of G) \ {v} c= v .allNeighbors()
for x being object st x in (the_Vertices_of G) \ {v} holds
x in v .allNeighbors() by A1;
hence (the_Vertices_of G) \ {v} c= v .allNeighbors() by TARSKI:def 3; :: thesis: verum