let G be loopless _Graph; :: thesis:
let v be Vertex of G; :: thesis:

now :: thesis:

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

end;

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

now :: thesis:

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

end;

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

now :: thesis:

let x be object ; :: thesis:
assume A3: x in v .allNeighbors() ; :: thesis:
then ex e being object st e Joins v,x,G by GLIB_000:71;
then v <> x by GLIB_000:18;
hence x in (the_Vertices_of G) \ {v} by A3, ZFMISC_1:56; :: thesis:

end;

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