theorem :: GLIB_006:73

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