let G be _Graph; :: thesis: G is inducedSubgraph of G,(the_Vertices_of G)
set V = the_Vertices_of G;
set E = the_Edges_of G;
( not the_Vertices_of G is empty & the_Vertices_of G c= the_Vertices_of G ) ;
then A2: the_Vertices_of G is non empty Subset of (the_Vertices_of G) ;
A3: G is Subgraph of G by GLIB_000:40;
the_Edges_of G c= G .edgesBetween (the_Vertices_of G) by GLIB_000:34;
then G is inducedSubgraph of G, the_Vertices_of G, the_Edges_of G by A2, A3, GLIB_000:def 37;
hence G is inducedSubgraph of G,(the_Vertices_of G) by GLIB_000:34; :: thesis: verum