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 v .edgesIn() c= {v} |` E
let E be symmetric Relation of V; :: thesis: for G being GraphFromSymRel of V,E
for v being Vertex of G holds v .edgesIn() c= {v} |` E
let G be GraphFromSymRel of V,E; :: thesis: for v being Vertex of G holds v .edgesIn() c= {v} |` E
let v be Vertex of G; :: thesis: v .edgesIn() c= {v} |` E
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;
v0 .edgesIn() = {v} |` E by Th79;
hence v .edgesIn() c= {v} |` E by GLIB_000:78; :: thesis: verum