let G be _Graph; :: thesis: (G .allInducedSG()) /\ (G .allSpanningSG()) = {(G | _GraphSelectors)}

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

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

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

assume x in (G .allInducedSG()) /\ (G .allSpanningSG()) ; :: thesis: x = G | _GraphSelectors
then A1: ( x in G .allInducedSG() & x in G .allSpanningSG() ) by XBOOLE_0:def 4;
then consider V being non empty Subset of (the_Vertices_of G) such that
A2: x is plain inducedSubgraph of G,V by Th45;
reconsider H = x as plain inducedSubgraph of G,V by A2;
A3: H is spanning by A1, Th60;
then A4: the_Vertices_of G = the_Vertices_of H by GLIB_000:def 33
.= V by GLIB_000:def 37 ;
the_Edges_of G = G .edgesBetween (the_Vertices_of G) by GLIB_000:34
.= the_Edges_of H by A4, GLIB_000:def 37 ;
then ( G == H & G == G | _GraphSelectors ) by A3, 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 .allInducedSG()) /\ (G .allSpanningSG())
then ( x in G .allInducedSG() & x in G .allSpanningSG() ) by Th47, Th62;
hence x in (G .allInducedSG()) /\ (G .allSpanningSG()) by XBOOLE_0:def 4; :: thesis: verum

end;

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