let G be _Graph; :: thesis: for W being Walk of G holds

( not W is trivial iff len W <> 1 )

let W be Walk of G; :: thesis: ( not W is trivial iff len W <> 1 )

A1: 1 <= len W by ABIAN:12;

thus ( not W is trivial implies len W <> 1 ) by Lm54; :: thesis: ( len W <> 1 implies not W is trivial )

assume len W <> 1 ; :: thesis: not 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 not W is trivial by Lm54; :: thesis: verum

( not W is trivial iff len W <> 1 )

let W be Walk of G; :: thesis: ( not W is trivial iff len W <> 1 )

A1: 1 <= len W by ABIAN:12;

thus ( not W is trivial implies len W <> 1 ) by Lm54; :: thesis: ( len W <> 1 implies not W is trivial )

assume len W <> 1 ; :: thesis: not 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 not W is trivial by Lm54; :: thesis: verum