theorem :: GLPACY00:26

for P being non _trivial Path-like _Graph holds
( ( P .order() = 2 implies P .maxDegree() = 1 ) & ( P .maxDegree() = 1 implies P .order() = 2 ) & ( P .order() <> 2 implies P .maxDegree() = 2 ) & ( P .maxDegree() = 2 implies P .order() <> 2 ) ) by Lm7;