let G be non edgeless _Graph; :: thesis: for e being Edge of G
for H being plain addVertices of createGraph e, the_Vertices_of G holds H in G .allSpanningSG()
let e be Edge of G; :: thesis: for H being plain addVertices of createGraph e, the_Vertices_of G holds H in G .allSpanningSG()
let H be plain addVertices of createGraph e, the_Vertices_of G; :: thesis: H in G .allSpanningSG()
A1: the_Vertices_of H = (the_Vertices_of (createGraph e)) \/ (the_Vertices_of G) by GLIB_006:def 10
.= the_Vertices_of G by XBOOLE_1:12 ;
the_Vertices_of G c= the_Vertices_of G ;
then H is spanning Subgraph of G by A1, Th21, GLIB_000:def 33;
hence H in G .allSpanningSG() by Th60; :: thesis: verum