let G be _Graph; :: thesis:
let x be set ; :: thesis:
let v be Vertex of G; :: thesis:

hereby :: thesis:

assume A1: x in v .allNeighbors() ; :: thesis:

now :: thesis:

per cases by A1, XBOOLE_0:def 3;

suppose x in v .inNeighbors() ; :: thesis:

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

end;

suppose x in v .outNeighbors() ; :: thesis:

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

end;

end;

end;

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

end;

given e being object such that A4: e Joins v,x,G ; :: thesis:

now :: thesis:

per cases by A4;

suppose e DJoins x,v,G ; :: thesis:

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

end;

suppose e DJoins v,x,G ; :: thesis:

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

end;

end;

end;

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