let G1, G2 be _Graph; :: thesis: for F being semi-continuous PGraphMapping of G1,G2 st dom (F _E) = the_Edges_of G1 & rng (F _E) = the_Edges_of G2 holds
F _V is continuous PVertexMapping of G1,G2
let F be semi-continuous PGraphMapping of G1,G2; :: thesis: ( dom (F _E) = the_Edges_of G1 & rng (F _E) = the_Edges_of G2 implies F _V is continuous PVertexMapping of G1,G2 )
assume A1: ( dom (F _E) = the_Edges_of G1 & rng (F _E) = the_Edges_of G2 ) ; :: thesis: F _V is continuous PVertexMapping of G1,G2
then A2: F _V is PVertexMapping of G1,G2 by Th17;

now :: thesis: for v, w being Vertex of G1 st v in dom (F _V) & w in dom (F _V) & (F _V) /. v,(F _V) /. w are_adjacent holds
ex e being object st
( e in rng (F _E) & e Joins (F _V) . v,(F _V) . w,G2 )

let v, w be Vertex of G1; :: thesis: ( v in dom (F _V) & w in dom (F _V) & (F _V) /. v,(F _V) /. w are_adjacent implies ex e being object st
( e in rng (F _E) & e Joins (F _V) . v,(F _V) . w,G2 ) )
assume A3: ( v in dom (F _V) & w in dom (F _V) & (F _V) /. v,(F _V) /. w are_adjacent ) ; :: thesis: ex e being object st
( e in rng (F _E) & e Joins (F _V) . v,(F _V) . w,G2 )
then consider e being object such that
A4: e Joins (F _V) /. v,(F _V) /. w,G2 by CHORD:def 3;
take e = e; :: thesis: ( e in rng (F _E) & e Joins (F _V) . v,(F _V) . w,G2 )
thus e in rng (F _E) by A1, A4, GLIB_000:def 13; :: thesis: e Joins (F _V) . v,(F _V) . w,G2
e Joins (F _V) . v,(F _V) /. w,G2 by A3, A4, PARTFUN1:def 6;
hence e Joins (F _V) . v,(F _V) . w,G2 by A3, PARTFUN1:def 6; :: thesis: verum

end;

hence F _V is continuous PVertexMapping of G1,G2 by A2, Th22; :: thesis: verum