let P be _finite non _trivial Path-like _Graph; :: thesis: card (Endvertices P) = 2
consider v1, v2 being Vertex of P such that
A1: ( v1 <> v2 & Endvertices P = {v1,v2} ) by Th36;
thus card (Endvertices P) = 2 by A1, CARD_2:57; :: thesis: verum