let v be Vertex of G; :: thesis: v is endvertex
v .degree() = 1 by Def4;
hence v is endvertex by GLIB_000:174; :: thesis: verum