theorem :: GLIB_008:20

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