for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for X, Y being Subset of (the_Vertices_of G1) st F is weak_SG-embedding holds
card (G1 .edgesBetween (X,Y)) c= card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)))