let G be _Graph; :: thesis: for v being Vertex of G holds Im ((VertexAdjSymRel G),v) = v .allNeighbors()
let v be Vertex of G; :: thesis: Im ((VertexAdjSymRel G),v) = v .allNeighbors()

now :: thesis: for x being object holds
( ( x in (VertexAdjSymRel G) .: {v} implies x in v .allNeighbors() ) & ( x in v .allNeighbors() implies x in (VertexAdjSymRel G) .: {v} ) )

let x be object ; :: thesis: ( ( x in (VertexAdjSymRel G) .: {v} implies x in v .allNeighbors() ) & ( x in v .allNeighbors() implies x in (VertexAdjSymRel G) .: {v} ) )

hereby :: thesis: ( x in v .allNeighbors() implies x in (VertexAdjSymRel G) .: {v} )

assume x in (VertexAdjSymRel G) .: {v} ; :: thesis: x in v .allNeighbors()
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: verum

end;

assume x in v .allNeighbors() ; :: thesis: x in (VertexAdjSymRel G) .: {v}
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: verum

end;

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