let G be _Graph; :: thesis: for W being Walk of G holds
( W is V5() iff len W <> 1 )
let W be Walk of G; :: thesis: ( W is V5() iff len W <> 1 )
A1: 1 <= len W by ABIAN:12;
thus ( W is V5() implies len W <> 1 ) by Lm54; :: thesis: ( len W <> 1 implies not W is V5() )
assume len W <> 1 ; :: thesis: W is V5()
then 1 < len W by A1, XXREAL_0:1;
then 1 + 1 <= len W by NAT_1:13;
then 2 * 1 < len W by XXREAL_0:1;
then (2 * 1) + 1 <= len W by NAT_1:13;
hence W is V5() by Lm54; :: thesis: verum