let V be non empty set ; :: thesis: for E being Relation of V
for v being Vertex of (createGraph (V,E)) holds Coim (E,v) = v .inNeighbors()
let E be Relation of V; :: thesis: for v being Vertex of (createGraph (V,E)) holds Coim (E,v) = v .inNeighbors()
let v be Vertex of (createGraph (V,E)); :: thesis: Coim (E,v) = v .inNeighbors()

now :: thesis: for x being object holds
( ( x in Coim (E,v) implies x in v .inNeighbors() ) & ( x in v .inNeighbors() implies x in Coim (E,v) ) )

let x be object ; :: thesis: ( ( x in Coim (E,v) implies x in v .inNeighbors() ) & ( x in v .inNeighbors() implies x in Coim (E,v) ) )

hereby :: thesis: ( x in v .inNeighbors() implies x in Coim (E,v) )

assume x in Coim (E,v) ; :: thesis: x in v .inNeighbors()
then x in E " {v} by RELAT_1:def 17;
then consider y being object such that
A1: ( [x,y] in E & y in {v} ) by RELAT_1:def 14;
y = v by A1, TARSKI:def 1;
then A2: [x,y] DJoins x,v, createGraph (V,E) by A1, Th63;
x is set by TARSKI:1;
hence x in v .inNeighbors() by A2, GLIB_000:69; :: thesis: verum

end;

assume x in v .inNeighbors() ; :: thesis: x in Coim (E,v)
then consider e being object such that
A3: e DJoins x,v, createGraph (V,E) by GLIB_000:69;
e = [x,v] by A3, Th64;
then A4: [x,v] in E by A3, Th63;
v in {v} by TARSKI:def 1;
then x in E " {v} by A4, RELAT_1:def 14;
hence x in Coim (E,v) by RELAT_1:def 17; :: thesis: verum

end;

hence Coim (E,v) = v .inNeighbors() by TARSKI:2; :: thesis: verum