let G1, G2 be _Graph; 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; ( F is weak_SG-embedding implies ( G1 .order() c= G2 .order() & G1 .size() c= G2 .size() ) )
assume
F is weak_SG-embedding
; ( 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; 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; verum