set G2 = the inducedSubgraph of G,{ the Vertex of G};
reconsider G3 = the removeEdges of the inducedSubgraph of G,{ the Vertex of G},(the_Edges_of the inducedSubgraph of G,{ the Vertex of G}) as Subgraph of G by GLIB_000:43;
take G3 ; :: thesis: ( G3 is edgeless & G3 is _trivial )
thus ( G3 is edgeless & G3 is _trivial ) ; :: thesis: verum