theorem :: GLENUM00:76

for G being _Graph holds the_Edges_of (G .allSpanningSG()) = bool (the_Edges_of G)