let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2
for X being Subset of (the_Vertices_of G1) st F is weak_SG-embedding holds
card (G1 .edgesBetween X) c= card (G2 .edgesBetween ((F _V) .: X))
let F be PGraphMapping of G1,G2; :: thesis: for X being Subset of (the_Vertices_of G1) st F is weak_SG-embedding holds
card (G1 .edgesBetween X) c= card (G2 .edgesBetween ((F _V) .: X))
let X be Subset of (the_Vertices_of G1); :: thesis: ( F is weak_SG-embedding implies card (G1 .edgesBetween X) c= card (G2 .edgesBetween ((F _V) .: X)) )
assume A1: F is weak_SG-embedding ; :: thesis: card (G1 .edgesBetween X) c= card (G2 .edgesBetween ((F _V) .: X))
set f = (F _E) | (G1 .edgesBetween X);
A2: dom ((F _E) | (G1 .edgesBetween X)) = (dom (F _E)) /\ (G1 .edgesBetween X) by RELAT_1:61
.= (the_Edges_of G1) /\ (G1 .edgesBetween X) by A1, Def11
.= G1 .edgesBetween X by XBOOLE_1:28 ;
for y being object st y in rng ((F _E) | (G1 .edgesBetween X)) holds
y in G2 .edgesBetween ((F _V) .: X)

proof

let y be object ; :: thesis: ( y in rng ((F _E) | (G1 .edgesBetween X)) implies y in G2 .edgesBetween ((F _V) .: X) )
assume y in rng ((F _E) | (G1 .edgesBetween X)) ; :: thesis: y in G2 .edgesBetween ((F _V) .: X)
then consider x being object such that
A3: ( x in dom ((F _E) | (G1 .edgesBetween X)) & ((F _E) | (G1 .edgesBetween X)) . x = y ) by FUNCT_1:def 3;
set v = (the_Source_of G1) . x;
set w = (the_Target_of G1) . x;
A4: ( x in the_Edges_of G1 & (the_Source_of G1) . x in X & (the_Target_of G1) . x in X ) by A2, A3, GLIB_000:31;
then ( (the_Source_of G1) . x in the_Vertices_of G1 & (the_Target_of G1) . x in the_Vertices_of G1 ) ;
then A5: ( (the_Source_of G1) . x in dom (F _V) & (the_Target_of G1) . x in dom (F _V) ) by A1, Def11;
A6: x in dom (F _E) by A1, A4, Def11;
x Joins (the_Source_of G1) . x,(the_Target_of G1) . x,G1 by A4, GLIB_000:def 13;
then (F _E) . x Joins (F _V) . ((the_Source_of G1) . x),(F _V) . ((the_Target_of G1) . x),G2 by A5, A6, Th4;
then A7: y Joins (F _V) . ((the_Source_of G1) . x),(F _V) . ((the_Target_of G1) . x),G2 by A3, FUNCT_1:47;
( (F _V) . ((the_Source_of G1) . x) in (F _V) .: X & (F _V) . ((the_Target_of G1) . x) in (F _V) .: X ) by A4, A5, FUNCT_1:def 6;
hence y in G2 .edgesBetween ((F _V) .: X) by A7, GLIB_000:32; :: thesis: verum

end;

then A8: rng ((F _E) | (G1 .edgesBetween X)) c= G2 .edgesBetween ((F _V) .: X) by TARSKI:def 3;
(F _E) | (G1 .edgesBetween X) is one-to-one by A1, FUNCT_1:52;
hence card (G1 .edgesBetween X) c= card (G2 .edgesBetween ((F _V) .: X)) by A2, A8, CARD_1:10; :: thesis: verum