set E1 = the RepEdgeSelection of G1;
set E2 = the RepEdgeSelection of G2;
consider F being PGraphMapping of G1,G2 such that
A1:
( F _V = f & dom (F _E) = the RepEdgeSelection of G1 /\ (G1 .edgesBetween (dom f)) & rng (F _E) c= the RepEdgeSelection of G2 /\ (G2 .edgesBetween (rng f)) )
by Th27;
take
F
; ( F _V = f & dom (F _E) = G1 .edgesBetween (dom f) & rng (F _E) c= G2 .edgesBetween (rng f) )
thus
F _V = f
by A1; ( dom (F _E) = G1 .edgesBetween (dom f) & rng (F _E) c= G2 .edgesBetween (rng f) )
A2:
( the RepEdgeSelection of G1 = the_Edges_of G1 & the RepEdgeSelection of G2 = the_Edges_of G2 )
by GLIB_009:74;
hence
dom (F _E) = G1 .edgesBetween (dom f)
by A1, XBOOLE_1:28; rng (F _E) c= G2 .edgesBetween (rng f)
thus
rng (F _E) c= G2 .edgesBetween (rng f)
by A1, A2, XBOOLE_1:28; verum