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

( not W is trivial iff 3 <= len W )

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

then (2 * 1) + 1 <= (2 * (len (W .edgeSeq()))) + 1 by Def15;

then W .length() <> 0 ;

hence not W is trivial ; :: thesis: verum

( not W is trivial iff 3 <= len W )

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

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

assume
3 <= len W
; :: thesis: not W is trivial assume
not 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;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

then (2 * 1) + 1 <= (2 * (len (W .edgeSeq()))) + 1 by Def15;

then W .length() <> 0 ;

hence not W is trivial ; :: thesis: verum