let n be Nat; :: thesis: for P1, P2 being n -edge Path-like _Graph holds P2 is P1 -isomorphic
let P1, P2 be n -edge Path-like _Graph; :: thesis: P2 is P1 -isomorphic
( P1 .size() = n & P2 .size() = n ) by GLIB_013:def 4;
then ( P1 .order() = n + 1 & P2 .order() = n + 1 ) by GLIB_002:46;
then ( P1 is n + 1 -vertex & P2 is n + 1 -vertex ) by GLIB_013:def 3;
hence P2 is P1 -isomorphic by Th32; :: thesis: verum