assume not Endvertices G is empty ; :: thesis: contradiction
then consider x being object such that
A1: x in Endvertices G by XBOOLE_0:def 1;
reconsider x = x as Vertex of G by A1;
thus contradiction by A1, GLIB_006:56; :: thesis: verum