theorem Th12: :: GLIB_001:13

for G being _Graph
for v being Vertex of G holds
( len (G .walkOf v) = 1 & (G .walkOf v) . 1 = v & (G .walkOf v) .first() = v & (G .walkOf v) .last() = v & G .walkOf v is_Walk_from v,v )