let G be _Graph; :: thesis: ( G is edgeless iff G .allSG() = { (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 .allSG() = { (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 .allSG() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum }

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

let x be object ; :: thesis: ( ( x in G .allSG() implies x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } ) & ( x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } implies x in G .allSG() ) )

hereby :: thesis: ( x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } implies x in G .allSG() )

assume x in G .allSG() ; :: thesis: x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum }
then reconsider H = x as plain Subgraph of G by Th1;
reconsider V = [#] (the_Vertices_of H) as non empty Subset of (the_Vertices_of G) ;
H == createGraph ([#] (the_Vertices_of H)) by A1, Th7;
then H = createGraph V by GLIB_009:44;
hence x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } ; :: thesis: verum

end;

assume x in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } ; :: thesis: x in G .allSG()
then consider V being non empty Subset of (the_Vertices_of G) such that
A2: x = createGraph V ;
thus x in G .allSG() by A2, Th4; :: thesis: verum

end;

hence G .allSG() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } by TARSKI:2; :: thesis: verum

end;

assume G .allSG() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } ; :: thesis: G is edgeless
then G | _GraphSelectors in { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } by Th3;
then consider V being non empty Subset of (the_Vertices_of G) such that
A3: G | _GraphSelectors = createGraph V ;
G == G | _GraphSelectors by GLIB_000:128;
hence G is edgeless by A3, GLIB_008:52; :: thesis: verum