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