let G be _Graph; :: thesis: for W being Walk of G holds
( W is trivial iff len W <> 1 )
let W be Walk of G; :: thesis: ( W is trivial iff len W <> 1 )
A1: 1 <= len W by ABIAN:12;
thus ( W is trivial implies len W <> 1 ) by Lm54; :: thesis: ( len W <> 1 implies not W is trivial )
assume len W <> 1 ; :: thesis: W is trivial
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 trivial by Lm54; :: thesis: verum