theorem :: GLIB_001:135

for G being _Graph
for W being Walk of G st W is trivial holds
for v being Vertex of G st v in W .vertices() holds
not v is isolated