let G be _Graph; :: thesis: for W being Walk of G holds
( W is V5() iff 3 <= len W )
let W be Walk of G; :: thesis: ( W is V5() iff 3 <= len W )
hereby :: thesis: ( 3 <= len W implies not W is V5() )
assume W is V5() ; :: 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 V5()
then (2 * 1) + 1 <= (2 * (len (W .edgeSeq()))) + 1 by Def15;
then W .length() <> 0 ;
hence W is V5() ; :: thesis: verum