let G1, G2 be _Graph; :: thesis: 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)))

let F be PGraphMapping of G1,G2; :: thesis: 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)))

let X, Y be Subset of (the_Vertices_of G1); :: 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

.= (the_Edges_of G1) /\ (G1 .edgesBetween (X,Y)) by A1, Def11

.= 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))

(F _E) | (G1 .edgesBetween (X,Y)) is one-to-one by A1, FUNCT_1:52;

hence card (G1 .edgesBetween (X,Y)) c= card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))) by A2, A15, CARD_1:10; :: thesis: verum

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)))

let F be PGraphMapping of G1,G2; :: thesis: 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)))

let X, Y be Subset of (the_Vertices_of G1); :: 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

.= (the_Edges_of G1) /\ (G1 .edgesBetween (X,Y)) by A1, Def11

.= 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

then A15:
rng ((F _E) | (G1 .edgesBetween (X,Y))) c= G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))
by TARSKI:def 3;
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 = (the_Source_of G1) . x;

set w = (the_Target_of G1) . x;

A4: x SJoins X,Y,G1 by A2, A3, GLIB_000:def 30;

end;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 = (the_Source_of G1) . x;

set w = (the_Target_of G1) . x;

A4: x SJoins X,Y,G1 by A2, A3, GLIB_000:def 30;

per cases then
( ( (the_Source_of G1) . x in X & (the_Target_of G1) . x in Y ) or ( (the_Source_of G1) . x in Y & (the_Target_of G1) . x in X ) )
by GLIB_000:def 15;

end;

suppose A5:
( (the_Source_of G1) . x in X & (the_Target_of G1) . 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 & (the_Target_of G1) . x in the_Vertices_of G1 )
;

then A6: ( (the_Source_of G1) . x in dom (F _V) & (the_Target_of G1) . x in dom (F _V) ) by A1, Def11;

A7: x in the_Edges_of G1 by A4, GLIB_000:def 15;

then A8: x in dom (F _E) by A1, Def11;

x Joins (the_Source_of G1) . x,(the_Target_of G1) . x,G1 by A7, 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 A6, A8, Th4;

then A9: 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) .: Y ) by A5, A6, FUNCT_1:def 6;

then y SJoins (F _V) .: X,(F _V) .: Y,G2 by A9, GLIB_000:17;

hence y in G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)) by GLIB_000:def 30; :: thesis: verum

end;then A6: ( (the_Source_of G1) . x in dom (F _V) & (the_Target_of G1) . x in dom (F _V) ) by A1, Def11;

A7: x in the_Edges_of G1 by A4, GLIB_000:def 15;

then A8: x in dom (F _E) by A1, Def11;

x Joins (the_Source_of G1) . x,(the_Target_of G1) . x,G1 by A7, 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 A6, A8, Th4;

then A9: 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) .: Y ) by A5, A6, FUNCT_1:def 6;

then y SJoins (F _V) .: X,(F _V) .: Y,G2 by A9, GLIB_000:17;

hence y in G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)) by GLIB_000:def 30; :: thesis: verum

suppose A10:
( (the_Source_of G1) . x in Y & (the_Target_of G1) . 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 & (the_Target_of G1) . x in the_Vertices_of G1 )
;

then A11: ( (the_Source_of G1) . x in dom (F _V) & (the_Target_of G1) . x in dom (F _V) ) by A1, Def11;

A12: x in the_Edges_of G1 by A4, GLIB_000:def 15;

then A13: x in dom (F _E) by A1, Def11;

x Joins (the_Source_of G1) . x,(the_Target_of G1) . x,G1 by A12, 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 A11, A13, Th4;

then A14: 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) .: Y & (F _V) . ((the_Target_of G1) . x) in (F _V) .: X ) by A10, A11, FUNCT_1:def 6;

then y SJoins (F _V) .: X,(F _V) .: Y,G2 by A14, GLIB_000:17;

hence y in G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)) by GLIB_000:def 30; :: thesis: verum

end;then A11: ( (the_Source_of G1) . x in dom (F _V) & (the_Target_of G1) . x in dom (F _V) ) by A1, Def11;

A12: x in the_Edges_of G1 by A4, GLIB_000:def 15;

then A13: x in dom (F _E) by A1, Def11;

x Joins (the_Source_of G1) . x,(the_Target_of G1) . x,G1 by A12, 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 A11, A13, Th4;

then A14: 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) .: Y & (F _V) . ((the_Target_of G1) . x) in (F _V) .: X ) by A10, A11, FUNCT_1:def 6;

then y SJoins (F _V) .: X,(F _V) .: Y,G2 by A14, GLIB_000:17;

hence y in G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)) by GLIB_000:def 30; :: thesis: verum

(F _E) | (G1 .edgesBetween (X,Y)) is one-to-one by A1, FUNCT_1:52;

hence card (G1 .edgesBetween (X,Y)) c= card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))) by A2, A15, CARD_1:10; :: thesis: verum