let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2
for H being Subgraph of G2 holds (F _E) " (the_Edges_of H) c= G1 .edgesBetween ((F _V) " (the_Vertices_of H))
let F be PGraphMapping of G1,G2; :: thesis: for H being Subgraph of G2 holds (F _E) " (the_Edges_of H) c= G1 .edgesBetween ((F _V) " (the_Vertices_of H))
let H be Subgraph of G2; :: thesis: (F _E) " (the_Edges_of H) c= G1 .edgesBetween ((F _V) " (the_Vertices_of H))

now :: thesis: for x being object st x in (F _E) " (the_Edges_of H) holds
x in G1 .edgesBetween ((F _V) " (the_Vertices_of H))

let x be object ; :: thesis: ( x in (F _E) " (the_Edges_of H) implies x in G1 .edgesBetween ((F _V) " (the_Vertices_of H)) )
assume x in (F _E) " (the_Edges_of H) ; :: thesis: x in G1 .edgesBetween ((F _V) " (the_Vertices_of H))
then A1: ( x in dom (F _E) & (F _E) . x in the_Edges_of H ) by FUNCT_1:def 7;
set v = (the_Source_of G1) . x;
set w = (the_Target_of G1) . x;
A2: ( (the_Source_of G1) . x in dom (F _V) & (the_Target_of G1) . x in dom (F _V) ) by A1, GLIB_010:5;
A3: x Joins (the_Source_of G1) . x,(the_Target_of G1) . x,G1 by A1, 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 A1, A2, GLIB_010:4;
then (F _E) . x Joins (F _V) . ((the_Source_of G1) . x),(F _V) . ((the_Target_of G1) . x),H by A1, GLIB_000:73;
then ( (F _V) . ((the_Source_of G1) . x) in the_Vertices_of H & (F _V) . ((the_Target_of G1) . x) in the_Vertices_of H ) by GLIB_000:13;
then ( (the_Source_of G1) . x in (F _V) " (the_Vertices_of H) & (the_Target_of G1) . x in (F _V) " (the_Vertices_of H) ) by A2, FUNCT_1:def 7;
hence x in G1 .edgesBetween ((F _V) " (the_Vertices_of H)) by A3, GLIB_000:32; :: thesis: verum

end;

hence (F _E) " (the_Edges_of H) c= G1 .edgesBetween ((F _V) " (the_Vertices_of H)) by TARSKI:def 3; :: thesis: verum