let G be _Graph; :: thesis: for v being Vertex of G holds (G .walkOf v) .edges() = {}

let v be Vertex of G; :: thesis: (G .walkOf v) .edges() = {}

A1: (G .walkOf v) .edgeSeq() = <*> (the_Edges_of G) by Th24

.= {} ;

thus (G .walkOf v) .edges() = rng {} by A1, GLIB_001:def 17

.= {} ; :: thesis: verum

let v be Vertex of G; :: thesis: (G .walkOf v) .edges() = {}

A1: (G .walkOf v) .edgeSeq() = <*> (the_Edges_of G) by Th24

.= {} ;

thus (G .walkOf v) .edges() = rng {} by A1, GLIB_001:def 17

.= {} ; :: thesis: verum