let G be _Graph; :: thesis: for v being Vertex of G holds v .edgesInOut() = G .edgesBetween ((the_Vertices_of G),{v})
let v be Vertex of G; :: thesis: v .edgesInOut() = G .edgesBetween ((the_Vertices_of G),{v})
thus v .edgesInOut() = (v .edgesIn()) \/ (v .edgesOut())
.= (G .edgesDBetween ((the_Vertices_of G),{v})) \/ (v .edgesOut()) by GLIB_000:39
.= (G .edgesDBetween ((the_Vertices_of G),{v})) \/ (G .edgesDBetween ({v},(the_Vertices_of G))) by GLIB_000:39
.= G .edgesBetween ((the_Vertices_of G),{v}) by Th32 ; :: thesis: verum