consider v1, v2 being Vertex of G such that
v1 <> v2 and
A1: v1 is endvertex and
v2 is endvertex by Lm24;
take v1 ; :: thesis: v1 is endvertex
thus v1 is endvertex by A1; :: thesis: verum