let V be non empty set ; :: thesis: for E being Relation of V
for v being Vertex of (createGraph (V,E)) holds E | {v} = v .edgesOut()
let E be Relation of V; :: thesis: for v being Vertex of (createGraph (V,E)) holds E | {v} = v .edgesOut()
let v be Vertex of (createGraph (V,E)); :: thesis: E | {v} = v .edgesOut()
thus E | {v} = (createGraph (V,E)) .edgesOutOf {v} by Th74
.= v .edgesOut() by GLIB_000:def 39 ; :: thesis: verum