let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds

( G1 .order() c= G2 .order() & G1 .size() c= G2 .size() )

let F be PGraphMapping of G1,G2; :: thesis: ( F is weak_SG-embedding implies ( G1 .order() c= G2 .order() & G1 .size() c= G2 .size() ) )

assume F is weak_SG-embedding ; :: thesis: ( G1 .order() c= G2 .order() & G1 .size() c= G2 .size() )

then A1: ( dom (F _V) = the_Vertices_of G1 & dom (F _E) = the_Edges_of G1 & F _V is one-to-one & F _E is one-to-one ) by Def11;

( rng (F _V) c= the_Vertices_of G2 & rng (F _E) c= the_Edges_of G2 ) ;

then A2: ( card (the_Vertices_of G1) c= card (the_Vertices_of G2) & card (the_Edges_of G1) c= card (the_Edges_of G2) ) by A1, CARD_1:10;

then G1 .order() c= card (the_Vertices_of G2) by GLIB_000:def 24;

hence G1 .order() c= G2 .order() by GLIB_000:def 24; :: thesis: G1 .size() c= G2 .size()

G1 .size() c= card (the_Edges_of G2) by A2, GLIB_000:def 25;

hence G1 .size() c= G2 .size() by GLIB_000:def 25; :: thesis: verum

( G1 .order() c= G2 .order() & G1 .size() c= G2 .size() )

let F be PGraphMapping of G1,G2; :: thesis: ( F is weak_SG-embedding implies ( G1 .order() c= G2 .order() & G1 .size() c= G2 .size() ) )

assume F is weak_SG-embedding ; :: thesis: ( G1 .order() c= G2 .order() & G1 .size() c= G2 .size() )

then A1: ( dom (F _V) = the_Vertices_of G1 & dom (F _E) = the_Edges_of G1 & F _V is one-to-one & F _E is one-to-one ) by Def11;

( rng (F _V) c= the_Vertices_of G2 & rng (F _E) c= the_Edges_of G2 ) ;

then A2: ( card (the_Vertices_of G1) c= card (the_Vertices_of G2) & card (the_Edges_of G1) c= card (the_Edges_of G2) ) by A1, CARD_1:10;

then G1 .order() c= card (the_Vertices_of G2) by GLIB_000:def 24;

hence G1 .order() c= G2 .order() by GLIB_000:def 24; :: thesis: G1 .size() c= G2 .size()

G1 .size() c= card (the_Edges_of G2) by A2, GLIB_000:def 25;

hence G1 .size() c= G2 .size() by GLIB_000:def 25; :: thesis: verum