theorem Th13: :: GLIB_008:13

for G1 being finite _Graph
for G2 being spanning Subgraph of G1 st G1 .size() = G2 .size() holds
G1 == G2