theorem :: GLENUM00:30
for G1, G2 being _Graph holds
( G1 == G2 iff G1 .allSG() = G2 .allSG() )