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 & the_Vertices_of G c= the_Vertices_of G ) by Lm6;
then the_Vertices_of G1 = the_Vertices_of G by Def37;
hence G1 is spanning ; :: thesis: verum