let G be loopless complete _Graph; :: thesis: for v being Vertex of G holds v .allNeighbors() = (the_Vertices_of G) \ {v}
let v be Vertex of G; :: thesis: v .allNeighbors() = (the_Vertices_of G) \ {v}
now :: thesis: for x being object st x in v .allNeighbors() holds
x in (the_Vertices_of G) \ {v}
let x be object ; :: thesis: ( x in v .allNeighbors() implies x in (the_Vertices_of G) \ {v} )
assume A1: x in v .allNeighbors() ; :: thesis: x in (the_Vertices_of G) \ {v}
for e being object holds not e Joins v,v,G by GLIB_000:18;
then not v in v .allNeighbors() by GLIB_000:71;
then not x in {v} by A1, TARSKI:def 1;
hence x in (the_Vertices_of G) \ {v} by A1, XBOOLE_0:def 5; :: thesis: verum
end;
then A2: v .allNeighbors() c= (the_Vertices_of G) \ {v} by TARSKI:def 3;
(the_Vertices_of G) \ {v} c= v .allNeighbors() by Th44;
hence v .allNeighbors() = (the_Vertices_of G) \ {v} by A2, XBOOLE_0:def 10; :: thesis: verum