let G be _Graph; :: thesis: the_Vertices_of (G .allSpanningSG()) = {(the_Vertices_of G)}

now :: thesis: for x being object holds
( ( x in the_Vertices_of (G .allSpanningSG()) implies x = the_Vertices_of G ) & ( x = the_Vertices_of G implies x in the_Vertices_of (G .allSpanningSG()) ) )

let x be object ; :: thesis: ( ( x in the_Vertices_of (G .allSpanningSG()) implies x = the_Vertices_of G ) & ( x = the_Vertices_of G implies x in the_Vertices_of (G .allSpanningSG()) ) )

hereby :: thesis: ( x = the_Vertices_of G implies x in the_Vertices_of (G .allSpanningSG()) )

assume x in the_Vertices_of (G .allSpanningSG()) ; :: thesis: x = the_Vertices_of G
then consider H being _Graph such that
A1: ( H in G .allSpanningSG() & x = the_Vertices_of H ) by GLIB_014:def 14;
H is spanning Subgraph of G by A1, Th60;
hence x = the_Vertices_of G by A1, GLIB_000:def 33; :: thesis: verum

end;

assume A2: x = the_Vertices_of G ; :: thesis: x in the_Vertices_of (G .allSpanningSG())
set H = the spanning plain Subgraph of G;
( the spanning plain Subgraph of G in G .allSpanningSG() & the_Vertices_of the spanning plain Subgraph of G = the_Vertices_of G ) by Th60, GLIB_000:def 33;
hence x in the_Vertices_of (G .allSpanningSG()) by A2, GLIB_014:def 14; :: thesis: verum

end;

hence the_Vertices_of (G .allSpanningSG()) = {(the_Vertices_of G)} by TARSKI:def 1; :: thesis: verum