let G be _Graph; :: thesis: for x being set
for v being Vertex of G holds
( x in v .allNeighbors() iff ex e being set 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 set st e Joins v,x,G )
let v be Vertex of G; :: thesis: ( x in v .allNeighbors() iff ex e being set st e Joins v,x,G )

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

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

now

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 set st e Joins v,x,G

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

end;

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

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

end;

end;

end;

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

end;

assume ex e being set st e Joins v,x,G ; :: thesis: x in v .allNeighbors()
then consider e being set such that
A4: e Joins v,x,G ;

now

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

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

then x in v .inNeighbors() by Th72;
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 Th73;
hence x in (v .inNeighbors()) \/ (v .outNeighbors()) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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