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

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in (VertexAdjSymRel G) .: {v} ; :: thesis:
then consider v0 being object such that
A1: ( [v0,x] in VertexAdjSymRel G & v0 in {v} ) by RELAT_1:def 13;
[v,x] in VertexAdjSymRel G by A1, TARSKI:def 1;
then ( x is set & ex e being object st e Joins v,x,G ) by Th32, TARSKI:1;
hence x in v .allNeighbors() by GLIB_000:71; :: thesis:

end;

assume x in v .allNeighbors() ; :: thesis:
then ex e being object st e Joins v,x,G by GLIB_000:71;
then ( [v,x] in VertexAdjSymRel G & v in {v} ) by Th32, TARSKI:def 1;
hence x in (VertexAdjSymRel G) .: {v} by RELAT_1:def 13; :: thesis:

end;

then (VertexAdjSymRel G) .: {v} = v .allNeighbors() by TARSKI:2;
hence Im ((VertexAdjSymRel G),v) = v .allNeighbors() by RELAT_1:def 16; :: thesis: