let G be _Graph; :: thesis: the_Vertices_of (G .allSG()) = (bool (the_Vertices_of G)) \ {{}}

now :: thesis: for x being object holds
( ( x in the_Vertices_of (G .allSG()) implies x in (bool (the_Vertices_of G)) \ {{}} ) & ( x in (bool (the_Vertices_of G)) \ {{}} implies x in the_Vertices_of (G .allSG()) ) )

let x be object ; :: thesis: ( ( x in the_Vertices_of (G .allSG()) implies x in (bool (the_Vertices_of G)) \ {{}} ) & ( x in (bool (the_Vertices_of G)) \ {{}} implies x in the_Vertices_of (G .allSG()) ) )

hereby :: thesis: ( x in (bool (the_Vertices_of G)) \ {{}} implies x in the_Vertices_of (G .allSG()) )

assume x in the_Vertices_of (G .allSG()) ; :: thesis: x in (bool (the_Vertices_of G)) \ {{}}
then consider H being _Graph such that
A1: ( H in G .allSG() & x = the_Vertices_of H ) by GLIB_014:def 14;
H is Subgraph of G by A1, Th1;
then the_Vertices_of H c= the_Vertices_of G by GLIB_000:def 32;
then A2: x in bool (the_Vertices_of G) by A1;
not x in {{}} by A1, TARSKI:def 1;
hence x in (bool (the_Vertices_of G)) \ {{}} by A2, XBOOLE_0:def 5; :: thesis: verum

end;

reconsider X = x as set by TARSKI:1;
assume x in (bool (the_Vertices_of G)) \ {{}} ; :: thesis: x in the_Vertices_of (G .allSG())
then ( x in bool (the_Vertices_of G) & not x in {{}} ) by XBOOLE_0:def 5;
then reconsider X = X as non empty Subset of (the_Vertices_of G) by TARSKI:def 1;
set S = the Function of {},X;
set H = createGraph (X,{}, the Function of {},X, the Function of {},X);
( the_Vertices_of (createGraph (X,{}, the Function of {},X, the Function of {},X)) = X & createGraph (X,{}, the Function of {},X, the Function of {},X) in G .allSG() ) by Lm1;
hence x in the_Vertices_of (G .allSG()) by GLIB_014:def 14; :: thesis: verum

end;

hence the_Vertices_of (G .allSG()) = (bool (the_Vertices_of G)) \ {{}} by TARSKI:2; :: thesis: verum