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

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

let x be object ; :: thesis: ( x in v .inNeighbors() implies x in (the_Vertices_of G) \ {v} )
assume A1: x in v .inNeighbors() ; :: thesis: x in (the_Vertices_of G) \ {v}
then ex e being object st e DJoins x,v,G by Th69;
then v <> x by Th136;
hence x in (the_Vertices_of G) \ {v} by A1, ZFMISC_1:56; :: thesis: verum

end;

hence v .inNeighbors() c= (the_Vertices_of G) \ {v} ; :: thesis: ( v .outNeighbors() c= (the_Vertices_of G) \ {v} & v .allNeighbors() c= (the_Vertices_of G) \ {v} )

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

let x be object ; :: thesis: ( x in v .outNeighbors() implies x in (the_Vertices_of G) \ {v} )
assume A2: x in v .outNeighbors() ; :: thesis: x in (the_Vertices_of G) \ {v}
then ex e being object st e DJoins v,x,G by Th70;
then v <> x by Th136;
hence x in (the_Vertices_of G) \ {v} by A2, ZFMISC_1:56; :: thesis: verum

end;

hence v .outNeighbors() c= (the_Vertices_of G) \ {v} ; :: thesis: v .allNeighbors() c= (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 A3: x in v .allNeighbors() ; :: thesis: x in (the_Vertices_of G) \ {v}
then ex e being object st e Joins v,x,G by Th71;
then v <> x by Th18;
hence x in (the_Vertices_of G) \ {v} by A3, ZFMISC_1:56; :: thesis: verum

end;

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