reconsider G9 = G as Subgraph of G by Lm4;
take G9 ; :: thesis: G9 is spanning
the_Vertices_of G9 = the_Vertices_of G ;
hence G9 is spanning by Def35; :: thesis: verum