let G be _Graph; :: thesis: ( G is edgeless iff G .allInducedSG() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } )
set S = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } ;

hereby :: thesis: ( G .allInducedSG() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } implies G is edgeless )

assume A1: G is edgeless ; :: thesis: G .allInducedSG() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum }
G .allInducedSG() c= G .allSG() ;
then A2: G .allInducedSG() c= { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } by A1, Th9;

now :: thesis: for x being object st x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } holds
x in G .allInducedSG()

let x be object ; :: thesis: ( x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } implies x in G .allInducedSG() )
assume x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } ; :: thesis: x in G .allInducedSG()
then consider V being non empty Subset of (the_Vertices_of G) such that
A3: x = createGraph V ;
set H = createGraph V;
A4: G .edgesBetween V = the_Edges_of (createGraph V) by A1;
A5: the_Vertices_of (createGraph V) = V ;
createGraph V is inducedSubgraph of G,V by A4, A5, GLIB_000:def 37;
hence x in G .allInducedSG() by A3, Th45; :: thesis: verum

end;

then { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } c= G .allInducedSG() by TARSKI:def 3;
hence G .allInducedSG() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } by A2, XBOOLE_0:def 10; :: thesis: verum

end;

assume A6: G .allInducedSG() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } ; :: thesis: G is edgeless
G | _GraphSelectors in G .allInducedSG() by Th47;
then consider V being non empty Subset of (the_Vertices_of G) such that
A7: G | _GraphSelectors = createGraph V by A6;
A8: G == G | _GraphSelectors by GLIB_000:128;
the_Edges_of (G | _GraphSelectors) = {} by A7;
then the_Edges_of G = {} by A8, GLIB_000:def 34;
hence G is edgeless ; :: thesis: verum