theorem Th75: :: GLENUM00:75

for G being _Graph holds the_Vertices_of (G .allSpanningSG()) = {(the_Vertices_of G)}