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

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