theorem :: GLENUM00:66
for G1, G2 being _Graph holds
( G1 == G2 iff G1 .allSpanningSG() = G2 .allSpanningSG() )