let G be _Graph; :: thesis: createGraph ([#] (the_Vertices_of G)) in G .allSpanningSG()
set H = createGraph ([#] (the_Vertices_of G));
reconsider H = createGraph ([#] (the_Vertices_of G)) as Subgraph of G ;
the_Vertices_of H = the_Vertices_of G ;
then H is spanning by GLIB_000:def 33;
hence createGraph ([#] (the_Vertices_of G)) in G .allSpanningSG() by Th60; :: thesis: verum