theorem :: GLPACY00:25

for n being Nat
for P1, P2 being b₁ -edge Path-like _Graph holds P2 is P1 -isomorphic