let G be _Graph; :: thesis: for W being Walk of G holds
( W is trivial iff 3 <= len W )
let W be Walk of G; :: thesis: ( W is trivial iff 3 <= len W )

hereby :: thesis: ( 3 <= len W implies not W is trivial )

assume W is trivial ; :: thesis: 3 <= len W
then W .length() <> 0 ;
then 0 + 1 <= len (W .edgeSeq()) by NAT_1:13;
then 2 * 1 <= 2 * (len (W .edgeSeq())) by NAT_1:4;
then 2 + 1 <= (2 * (len (W .edgeSeq()))) + 1 by XREAL_1:7;
hence 3 <= len W by Def15; :: thesis: verum

end;

assume 3 <= len W ; :: thesis: W is trivial
then (2 * 1) + 1 <= (2 * (len (W .edgeSeq()))) + 1 by Def15;
then W .length() <> 0 ;
hence W is trivial ; :: thesis: verum