theorem Th31: :: GLPACY00:23

for P being _finite Path-like _Graph ex P0 being vertex-distinct Path of P st
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is trivial implies P is _trivial ) & ( P is _trivial implies P0 is trivial ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )