let P be Path-like _Graph; :: thesis: ( P .order() = 2 implies Endvertices P = the_Vertices_of P )
assume A1: P .order() = 2 ; :: thesis: Endvertices P = the_Vertices_of P
then consider v, w being object such that
A2: ( v <> w & the_Vertices_of P = {v,w} ) by CARD_2:60;
reconsider v = v, w = w as Vertex of P by A2, TARSKI:def 2;
A3: P is 2 -vertex by A1, GLIB_013:def 3;
for u being object st u in {v,w} holds
u in Endvertices P by A3, GLIB_006:56;
then {v,w} c= Endvertices P by TARSKI:def 3;
hence Endvertices P = the_Vertices_of P by A2, XBOOLE_0:def 10; :: thesis: verum