let G1 be inducedSubgraph of G, the_Vertices_of G,E; :: thesis: G1 is spanning
G .edgesBetween (the_Vertices_of G) = the_Edges_of G by Lm7;
then ( the_Vertices_of G c= the_Vertices_of G & E c= G .edgesBetween (the_Vertices_of G) ) ;
then the_Vertices_of G1 = the_Vertices_of G by Def39;
hence G1 is spanning by Def35; :: thesis: verum