theorem :: GLIB_006:74

for G2 being _finite _Graph
for G1 being _finite Supergraph of G2 holds
( G2 .order() <= G1 .order() & G2 .size() <= G1 .size() )