let V be non empty set ; :: thesis: for E being symmetric Relation of V
for G being GraphFromSymRel of V,E
for v being Vertex of G holds Im (E,v) = v .allNeighbors()
let E be symmetric Relation of V; :: thesis: for G being GraphFromSymRel of V,E
for v being Vertex of G holds Im (E,v) = v .allNeighbors()
let G be GraphFromSymRel of V,E; :: thesis: for v being Vertex of G holds Im (E,v) = v .allNeighbors()
let v be Vertex of G; :: thesis: Im (E,v) = v .allNeighbors()
set G0 = createGraph (V,E);
consider E0 being RepEdgeSelection of createGraph (V,E) such that
A1: G is inducedSubgraph of createGraph (V,E), the_Vertices_of (createGraph (V,E)),E0 by GLIB_009:def 7;
A2: the_Edges_of (createGraph (V,E)) = (createGraph (V,E)) .edgesBetween (the_Vertices_of (createGraph (V,E))) by GLIB_000:34;
the_Vertices_of (createGraph (V,E)) c= the_Vertices_of (createGraph (V,E)) ;
then reconsider v0 = v as Vertex of (createGraph (V,E)) by A1, A2, GLIB_000:def 37;
thus Im (E,v) = (Im (E,v)) \/ (Im (E,v))
.= (Im (E,v)) \/ (Coim (E,v)) by GLIBPRE0:10
.= (v0 .outNeighbors()) \/ (Coim (E,v)) by Th72
.= (v0 .outNeighbors()) \/ (v0 .inNeighbors()) by Th73
.= v0 .allNeighbors() by GLIB_000:def 48
.= v .allNeighbors() by GLIBPRE0:64 ; :: thesis: verum