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 )
thus ( not W is trivial implies len W <> 1 ) by Lm54; :: thesis: ( len W <> 1 implies not W is trivial )
assume A1: len W <> 1 ; :: thesis: not W is trivial
1 <= len W by HEYTING3:1;
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