let v be Vertex of G; :: thesis: ( v is isolated implies not v is endvertex )
assume A1: v is isolated ; :: thesis: not v is endvertex
assume v is endvertex ; :: thesis: contradiction
then consider e being object such that
A2: ( v .edgesInOut() = {e} & not e Joins v,v,G ) by GLIB_000:def 51;
thus contradiction by A1, A2, GLIB_000:def 49; :: thesis: verum