take the V5() Walk of G ; :: thesis: ( the V5() Walk of G is minlength & the V5() Walk of G is Path-like )
thus ( the V5() Walk of G is minlength & the V5() Walk of G is Path-like ) ; :: thesis: verum