let G be _Graph; :: thesis: the_Vertices_of (G .allInducedSG()) = (bool (the_Vertices_of G)) \ {{}}
the_Vertices_of (G .allInducedSG()) c= the_Vertices_of (G .allSG()) by GLIBPRE1:115;
then A1: the_Vertices_of (G .allInducedSG()) c= (bool (the_Vertices_of G)) \ {{}} by Th37;

now :: thesis: for x being object st x in (bool (the_Vertices_of G)) \ {{}} holds
x in the_Vertices_of (G .allInducedSG())

let x be object ; :: thesis: ( x in (bool (the_Vertices_of G)) \ {{}} implies x in the_Vertices_of (G .allInducedSG()) )
reconsider X = x as set by TARSKI:1;
assume x in (bool (the_Vertices_of G)) \ {{}} ; :: thesis: x in the_Vertices_of (G .allInducedSG())
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 H = the plain inducedSubgraph of G,X;
( the_Vertices_of the plain inducedSubgraph of G,X = X & the plain inducedSubgraph of G,X in G .allInducedSG() ) by GLIB_000:def 37;
hence x in the_Vertices_of (G .allInducedSG()) by GLIB_014:def 14; :: thesis: verum

end;

then (bool (the_Vertices_of G)) \ {{}} c= the_Vertices_of (G .allInducedSG()) by TARSKI:def 3;
hence the_Vertices_of (G .allInducedSG()) = (bool (the_Vertices_of G)) \ {{}} by A1, XBOOLE_0:def 10; :: thesis: verum