let G be _Graph; :: thesis: ( G is edgeless iff G .allSpanningSG() = {(G | _GraphSelectors)} )

hereby :: thesis: ( G .allSpanningSG() = {(G | _GraphSelectors)} implies G is edgeless )

assume A1: G is edgeless ; :: thesis: G .allSpanningSG() = {(G | _GraphSelectors)}

now :: thesis: for x being object holds
( ( x in G .allSpanningSG() implies x = G | _GraphSelectors ) & ( x = G | _GraphSelectors implies x in G .allSpanningSG() ) )

let x be object ; :: thesis: ( ( x in G .allSpanningSG() implies x = G | _GraphSelectors ) & ( x = G | _GraphSelectors implies x in G .allSpanningSG() ) )

hereby :: thesis: ( x = G | _GraphSelectors implies x in G .allSpanningSG() )

assume x in G .allSpanningSG() ; :: thesis: x = G | _GraphSelectors
then reconsider H = x as spanning plain Subgraph of G by Th60;
the_Edges_of H = {} by A1;
then the_Edges_of H = the_Edges_of G by A1;
then ( G == H & G == G | _GraphSelectors ) by GLIB_000:128, GLIB_000:118;
hence x = G | _GraphSelectors by GLIB_000:85, GLIB_009:44; :: thesis: verum

end;

assume x = G | _GraphSelectors ; :: thesis: x in G .allSpanningSG()
hence x in G .allSpanningSG() by Th62; :: thesis: verum

end;

hence G .allSpanningSG() = {(G | _GraphSelectors)} by TARSKI:def 1; :: thesis: verum

end;

assume A2: G .allSpanningSG() = {(G | _GraphSelectors)} ; :: thesis: G is edgeless
set H = the plain removeEdges of G,(the_Edges_of G);
the plain removeEdges of G,(the_Edges_of G) in G .allSpanningSG() by Th60;
then A3: the plain removeEdges of G,(the_Edges_of G) = G | _GraphSelectors by A2, TARSKI:def 1;
G == G | _GraphSelectors by GLIB_000:128;
then the_Edges_of G = the_Edges_of the plain removeEdges of G,(the_Edges_of G) by A3, GLIB_000:def 34
.= {} ;
hence G is edgeless ; :: thesis: verum