for G being _Graph
for W being Walk of G holds
( W is V5() iff 3 <= len W ) by Lm54;