theorem :: GLIB_006:56

for G being _Graph
for v being Vertex of G holds
( v in Endvertices G iff v is endvertex )