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 Lm3;
the_Edges_of G c= G .edgesBetween (the_Vertices_of G) by Th34;
then G is inducedSubgraph of G, the_Vertices_of G, the_Edges_of G by A2, A3, Def37;
hence G is inducedSubgraph of G,(the_Vertices_of G) by Th34; :: thesis: verum