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