theorem Th118: :: GLIB_000:118

for G1 being _Graph
for G2 being spanning Subgraph of G1 st the_Edges_of G1 = the_Edges_of G2 holds
G1 == G2