let V be non empty set ; :: thesis: for E being Relation of V
for v being Vertex of (createGraph (V,E)) holds Im (E,v) = v .outNeighbors()
let E be Relation of V; :: thesis: for v being Vertex of (createGraph (V,E)) holds Im (E,v) = v .outNeighbors()
let v be Vertex of (createGraph (V,E)); :: thesis: Im (E,v) = v .outNeighbors()
now :: thesis: for y being object holds
( ( y in Im (E,v) implies y in v .outNeighbors() ) & ( y in v .outNeighbors() implies y in Im (E,v) ) )
let y be object ; :: thesis: ( ( y in Im (E,v) implies y in v .outNeighbors() ) & ( y in v .outNeighbors() implies y in Im (E,v) ) )
hereby :: thesis: ( y in v .outNeighbors() implies y in Im (E,v) )
assume y in Im (E,v) ; :: thesis: y in v .outNeighbors()
then y in E .: {v} by RELAT_1:def 16;
then consider x being object such that
A1: ( [x,y] in E & x in {v} ) by RELAT_1:def 13;
x = v by A1, TARSKI:def 1;
then A2: [x,y] DJoins v,y, createGraph (V,E) by A1, Th63;
y is set by TARSKI:1;
hence y in v .outNeighbors() by A2, GLIB_000:70; :: thesis: verum
end;
assume y in v .outNeighbors() ; :: thesis: y in Im (E,v)
then consider e being object such that
A3: e DJoins v,y, createGraph (V,E) by GLIB_000:70;
e = [v,y] by A3, Th64;
then A4: [v,y] in E by A3, Th63;
v in {v} by TARSKI:def 1;
then y in E .: {v} by A4, RELAT_1:def 13;
hence y in Im (E,v) by RELAT_1:def 16; :: thesis: verum
end;
hence Im (E,v) = v .outNeighbors() by TARSKI:2; :: thesis: verum