let G2 be _Graph; :: thesis: for G1 being Supergraph of G2 holds
( G2 .order() c= G1 .order() & G2 .size() c= G1 .size() )
let G1 be Supergraph of G2; :: thesis: ( G2 .order() c= G1 .order() & G2 .size() c= G1 .size() )
( the_Vertices_of G2 c= the_Vertices_of G1 & the_Edges_of G2 c= the_Edges_of G1 ) by Def9;
then ( card (the_Vertices_of G2) c= card (the_Vertices_of G1) & card (the_Edges_of G2) c= card (the_Edges_of G1) ) by CARD_1:11;
then ( G2 .order() c= card (the_Vertices_of G1) & G2 .size() c= card (the_Edges_of G1) ) by GLIB_000:def 24, GLIB_000:def 25;
hence ( G2 .order() c= G1 .order() & G2 .size() c= G1 .size() ) by GLIB_000:def 24, GLIB_000:def 25; :: thesis: verum