take P = the n + 1 -vertex n -edge Path-like _Graph; :: thesis: ( P is n + 1 -vertex & P is n -edge & P is Path-like & not P is _trivial )
1 <= n by CHORD:1;
then 1 + 0 < n + 1 by XREAL_1:8;
then P .order() <> 1 by GLIB_013:def 3;
hence ( P is n + 1 -vertex & P is n -edge & P is Path-like & not P is _trivial ) by GLIB_013:def 3; :: thesis: verum