let V be non empty set ; :: thesis: for E being Relation of V
for v being Vertex of (createGraph (V,E)) holds {v} |` E = v .edgesIn()
let E be Relation of V; :: thesis: for v being Vertex of (createGraph (V,E)) holds {v} |` E = v .edgesIn()
let v be Vertex of (createGraph (V,E)); :: thesis: {v} |` E = v .edgesIn()
thus {v} |` E = (createGraph (V,E)) .edgesInto {v} by Th75
.= v .edgesIn() by GLIB_000:def 38 ; :: thesis: verum