theorem Th28: :: GLIBPRE1:28

for G being _Graph
for W being Walk of G st ( len W = 3 or W .length() = 1 ) holds
ex e being object st
( e Joins W .first() ,W .last() ,G & W = G .walkOf ((W .first()),e,(W .last())) )