let G1 be _finite _Graph; :: thesis: for G2 being Subgraph of G1 holds
( G2 .order() <= G1 .order() & G2 .size() <= G1 .size() )
let G2 be Subgraph of G1; :: thesis: ( G2 .order() <= G1 .order() & G2 .size() <= G1 .size() )
card (the_Vertices_of G2) <= card (the_Vertices_of G1) by NAT_1:43;
hence G2 .order() <= G1 .order() ; :: thesis: G2 .size() <= G1 .size()
card (the_Edges_of G2) <= card (the_Edges_of G1) by NAT_1:43;
hence G2 .size() <= G1 .size() ; :: thesis: verum