let G be complete _Graph; :: thesis: for v being Vertex of G holds (the_Vertices_of G) \ {v} c= v .allNeighbors()
let v be Vertex of G; :: thesis: (the_Vertices_of G) \ {v} c= v .allNeighbors()

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

let x be object ; :: thesis: ( x in (the_Vertices_of G) \ {v} implies x in v .allNeighbors() )
assume x in (the_Vertices_of G) \ {v} ; :: thesis: x in v .allNeighbors()
then A1: ( x in the_Vertices_of G & not x in {v} ) by XBOOLE_0:def 5;
then reconsider w = x as Vertex of G ;
v <> w by A1, TARSKI:def 1;
then ex e being object st e Joins v,w,G by CHORD:def 3, CHORD:def 6;
hence x in v .allNeighbors() by GLIB_000:71; :: thesis: verum

end;

hence (the_Vertices_of G) \ {v} c= v .allNeighbors() by TARSKI:def 3; :: thesis: verum