let G1, G2 be _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)))
let F be 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 X, Y be Subset of (the_Vertices_of G1); ( 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
; 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
let y be
object ;
( 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)))
;
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;
suppose A5:
(
(the_Source_of G1) . x in X &
(the_Target_of G1) . x in Y )
;
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;
verum end; suppose A10:
(
(the_Source_of G1) . x in Y &
(the_Target_of G1) . x in X )
;
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;
verum 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 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; verum