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

hereby :: thesis: ( G .allSG() = G .allInducedSG() implies G is edgeless )

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

end;

assume A2: G .allSG() = G .allInducedSG() ; :: thesis: G is edgeless
set H = createGraph ([#] (the_Vertices_of G));
consider V being non empty Subset of (the_Vertices_of G) such that
A3: createGraph ([#] (the_Vertices_of G)) is plain inducedSubgraph of G,V by A2, Lm1, Th45;
A4: V = the_Vertices_of (createGraph ([#] (the_Vertices_of G))) by A3, GLIB_000:def 37
.= the_Vertices_of G ;
{} = the_Edges_of (createGraph ([#] (the_Vertices_of G)))
.= G .edgesBetween V by A3, GLIB_000:def 37
.= the_Edges_of G by A4, GLIB_000:34 ;
hence G is edgeless ; :: thesis: verum