take P = the (n -' 1) + 1 -vertex n -' 1 -edge Path-like _Graph; :: thesis: ( P is n -vertex & P is n -' 1 -edge & P is Path-like )
1 - 1 <= n - 1 by CHORD:1, XREAL_1:9;
then (n -' 1) + 1 = n by NAT_D:72;
hence P is n -vertex ; :: thesis: ( P is n -' 1 -edge & P is Path-like )
thus ( P is n -' 1 -edge & P is Path-like ) ; :: thesis: verum