let G be _Graph; :: thesis: for x being set
for v being Vertex of G holds
( x in v .allNeighbors() iff ex e being object st e Joins v,x,G )
let x be set ; :: thesis: for v being Vertex of G holds
( x in v .allNeighbors() iff ex e being object st e Joins v,x,G )
let v be Vertex of G; :: thesis: ( x in v .allNeighbors() iff ex e being object st e Joins v,x,G )

hereby :: thesis: ( ex e being object st e Joins v,x,G implies x in v .allNeighbors() )

assume A1: x in v .allNeighbors() ; :: thesis: ex e being object st e Joins v,x,G

now :: thesis: ex e being object st e Joins v,x,G

per cases ( x in v .inNeighbors() or x in v .outNeighbors() ) by A1, XBOOLE_0:def 3;

suppose x in v .inNeighbors() ; :: thesis: ex e being object st e Joins v,x,G

then consider e being object such that
A2: e DJoins x,v,G by Th69;
take e = e; :: thesis: e Joins v,x,G
thus e Joins v,x,G by A2; :: thesis: verum

end;

suppose x in v .outNeighbors() ; :: thesis: ex e being object st e Joins v,x,G

then consider e being object such that
A3: e DJoins v,x,G by Th70;
take e = e; :: thesis: e Joins v,x,G
thus e Joins v,x,G by A3; :: thesis: verum

end;

end;

end;

hence ex e being object st e Joins v,x,G ; :: thesis: verum

end;

given e being object such that A4: e Joins v,x,G ; :: thesis: x in v .allNeighbors()

now :: thesis: x in (v .inNeighbors()) \/ (v .outNeighbors())

per cases ( e DJoins x,v,G or e DJoins v,x,G ) by A4;

suppose e DJoins x,v,G ; :: thesis: x in (v .inNeighbors()) \/ (v .outNeighbors())

then x in v .inNeighbors() by Th69;
hence x in (v .inNeighbors()) \/ (v .outNeighbors()) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose e DJoins v,x,G ; :: thesis: x in (v .inNeighbors()) \/ (v .outNeighbors())

then x in v .outNeighbors() by Th70;
hence x in (v .inNeighbors()) \/ (v .outNeighbors()) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in v .allNeighbors() ; :: thesis: verum