theorem Th65: :: GLENUM00:65

for G1, G2 being _Graph holds
( G2 .allSpanningSG() c= G1 .allSpanningSG() iff G2 is spanning Subgraph of G1 )