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