let P be _finite non _trivial Path-like _Graph; :: thesis: ex v1, v2 being Vertex of P st
( v1 <> v2 & Endvertices P = {v1,v2} )
consider P0 being vertex-distinct Path of P such that
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P ) and
A1: ( Endvertices P = {(P0 .first()),(P0 .last())} iff not P is _trivial ) and
( P0 is trivial iff P is _trivial ) and
A2: ( P0 is closed iff P is _trivial ) and
P0 is minlength by Th31;
take P0 .first() ; :: thesis: ex v2 being Vertex of P st
( P0 .first() <> v2 & Endvertices P = {(P0 .first()),v2} )
take P0 .last() ; :: thesis: ( P0 .first() <> P0 .last() & Endvertices P = {(P0 .first()),(P0 .last())} )
thus ( P0 .first() <> P0 .last() & Endvertices P = {(P0 .first()),(P0 .last())} ) by A1, A2, GLIB_001:def 24; :: thesis: verum