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