let G2 be _finite _Graph; :: thesis: for G1 being _finite Supergraph of G2 holds
( G2 .order() <= G1 .order() & G2 .size() <= G1 .size() )
let G1 be _finite Supergraph of G2; :: thesis: ( G2 .order() <= G1 .order() & G2 .size() <= G1 .size() )
G2 is Subgraph of G1 by Th61;
hence ( G2 .order() <= G1 .order() & G2 .size() <= G1 .size() ) by GLIB_000:75; :: thesis: verum