let G1 be inducedSubgraph of G, the_Vertices_of G, {} ; :: thesis: G1 is spanning
( the_Vertices_of G c= the_Vertices_of G & {} c= G .edgesBetween (the_Vertices_of G) ) by XBOOLE_1:2;
then the_Vertices_of G1 = the_Vertices_of G by Def39;
hence G1 is spanning by Def35; :: thesis: verum