let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2
for V being set holds (F _E) .: (G1 .edgesBetween V) c= G2 .edgesBetween ((F _V) .: V)
let F be PGraphMapping of G1,G2; :: thesis: for V being set holds (F _E) .: (G1 .edgesBetween V) c= G2 .edgesBetween ((F _V) .: V)
let V be set ; :: thesis: (F _E) .: (G1 .edgesBetween V) c= G2 .edgesBetween ((F _V) .: V)

now :: thesis: for e being object st e in (F _E) .: (G1 .edgesBetween V) holds
e in G2 .edgesBetween ((F _V) .: V)

let e be object ; :: thesis: ( e in (F _E) .: (G1 .edgesBetween V) implies e in G2 .edgesBetween ((F _V) .: V) )
assume e in (F _E) .: (G1 .edgesBetween V) ; :: thesis: e in G2 .edgesBetween ((F _V) .: V)
then consider e0 being object such that
A1: ( e0 in dom (F _E) & e0 in G1 .edgesBetween V & (F _E) . e0 = e ) by FUNCT_1:def 6;
set v0 = (the_Source_of G1) . e0;
set w0 = (the_Target_of G1) . e0;
A2: ( (the_Source_of G1) . e0 in dom (F _V) & (the_Target_of G1) . e0 in dom (F _V) ) by A1, GLIB_010:5;
e0 Joins (the_Source_of G1) . e0,(the_Target_of G1) . e0,G1 by A1, GLIB_000:def 13;
then A3: e Joins (F _V) . ((the_Source_of G1) . e0),(F _V) . ((the_Target_of G1) . e0),G2 by A1, A2, GLIB_010:4;
( (the_Source_of G1) . e0 in V & (the_Target_of G1) . e0 in V ) by A1, GLIB_000:31;
then ( (F _V) . ((the_Source_of G1) . e0) in (F _V) .: V & (F _V) . ((the_Target_of G1) . e0) in (F _V) .: V ) by A2, FUNCT_1:def 6;
hence e in G2 .edgesBetween ((F _V) .: V) by A3, GLIB_000:32; :: thesis: verum

end;

hence (F _E) .: (G1 .edgesBetween V) c= G2 .edgesBetween ((F _V) .: V) by TARSKI:def 3; :: thesis: verum