let G be _Graph; :: thesis: for v being Vertex of G holds Coim ((VertexDomRel G),v) = v .inNeighbors()
let v be Vertex of G; :: thesis: Coim ((VertexDomRel G),v) = v .inNeighbors()

now :: thesis: for x being object holds
( ( x in (VertexDomRel G) " {v} implies x in v .inNeighbors() ) & ( x in v .inNeighbors() implies x in (VertexDomRel G) " {v} ) )

let x be object ; :: thesis: ( ( x in (VertexDomRel G) " {v} implies x in v .inNeighbors() ) & ( x in v .inNeighbors() implies x in (VertexDomRel G) " {v} ) )

hereby :: thesis: ( x in v .inNeighbors() implies x in (VertexDomRel G) " {v} )

assume x in (VertexDomRel G) " {v} ; :: thesis: x in v .inNeighbors()
then consider v0 being object such that
A1: ( [x,v0] in VertexDomRel G & v0 in {v} ) by RELAT_1:def 14;
[x,v] in VertexDomRel G by A1, TARSKI:def 1;
then ( x is set & ex e being object st e DJoins x,v,G ) by Th1, TARSKI:1;
hence x in v .inNeighbors() by GLIB_000:69; :: thesis: verum

end;

assume x in v .inNeighbors() ; :: thesis: x in (VertexDomRel G) " {v}
then ex e being object st e DJoins x,v,G by GLIB_000:69;
then ( [x,v] in VertexDomRel G & v in {v} ) by Th1, TARSKI:def 1;
hence x in (VertexDomRel G) " {v} by RELAT_1:def 14; :: thesis: verum

end;

then (VertexDomRel G) " {v} = v .inNeighbors() by TARSKI:2;
hence Coim ((VertexDomRel G),v) = v .inNeighbors() by RELAT_1:def 17; :: thesis: verum