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

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in (VertexDomRel G) " {v} ; :: thesis:
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:

end;

assume x in v .inNeighbors() ; :: thesis:
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:

end;

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