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

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

let X, Y be Subset of (); :: thesis: ( F is weak_SG-embedding implies card (G1 .edgesBetween (X,Y)) c= card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))) )
assume A1: F is weak_SG-embedding ; :: thesis: card (G1 .edgesBetween (X,Y)) c= card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)))
set f = (F _E) | (G1 .edgesBetween (X,Y));
A2: dom ((F _E) | (G1 .edgesBetween (X,Y))) = (dom (F _E)) /\ (G1 .edgesBetween (X,Y)) by RELAT_1:61
.= () /\ (G1 .edgesBetween (X,Y)) by
.= G1 .edgesBetween (X,Y) by XBOOLE_1:28 ;
for y being object st y in rng ((F _E) | (G1 .edgesBetween (X,Y))) holds
y in G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))
proof
let y be object ; :: thesis: ( y in rng ((F _E) | (G1 .edgesBetween (X,Y))) implies y in G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)) )
assume y in rng ((F _E) | (G1 .edgesBetween (X,Y))) ; :: thesis: y in G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))
then consider x being object such that
A3: ( x in dom ((F _E) | (G1 .edgesBetween (X,Y))) & ((F _E) | (G1 .edgesBetween (X,Y))) . x = y ) by FUNCT_1:def 3;
set v = () . x;
set w = () . x;
A4: x SJoins X,Y,G1 by ;
per cases ) . x in X & () . x in Y ) or ( () . x in Y & () . x in X ) ) by GLIB_000:def 15;
suppose A5: ( (the_Source_of G1) . x in X & () . x in Y ) ; :: thesis: y in G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))
then ( (the_Source_of G1) . x in the_Vertices_of G1 & () . x in the_Vertices_of G1 ) ;
then A6: ( (the_Source_of G1) . x in dom (F _V) & () . x in dom (F _V) ) by ;
A7: x in the_Edges_of G1 by ;
then A8: x in dom (F _E) by ;
x Joins () . x,() . x,G1 by ;
then (F _E) . x Joins (F _V) . (() . x),(F _V) . (() . x),G2 by A6, A8, Th4;
then A9: y Joins (F _V) . (() . x),(F _V) . (() . x),G2 by ;
( (F _V) . (() . x) in (F _V) .: X & (F _V) . (() . x) in (F _V) .: Y ) by ;
then y SJoins (F _V) .: X,(F _V) .: Y,G2 by ;
hence y in G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)) by GLIB_000:def 30; :: thesis: verum
end;
suppose A10: ( (the_Source_of G1) . x in Y & () . x in X ) ; :: thesis: y in G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))
then ( (the_Source_of G1) . x in the_Vertices_of G1 & () . x in the_Vertices_of G1 ) ;
then A11: ( (the_Source_of G1) . x in dom (F _V) & () . x in dom (F _V) ) by ;
A12: x in the_Edges_of G1 by ;
then A13: x in dom (F _E) by ;
x Joins () . x,() . x,G1 by ;
then (F _E) . x Joins (F _V) . (() . x),(F _V) . (() . x),G2 by ;
then A14: y Joins (F _V) . (() . x),(F _V) . (() . x),G2 by ;
( (F _V) . (() . x) in (F _V) .: Y & (F _V) . (() . x) in (F _V) .: X ) by ;
then y SJoins (F _V) .: X,(F _V) .: Y,G2 by ;
hence y in G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)) by GLIB_000:def 30; :: thesis: verum
end;
end;
end;
then A15: rng ((F _E) | (G1 .edgesBetween (X,Y))) c= G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)) by TARSKI:def 3;
(F _E) | (G1 .edgesBetween (X,Y)) is one-to-one by ;
hence card (G1 .edgesBetween (X,Y)) c= card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))) by ; :: thesis: verum