let G1, G2 be _Graph; :: thesis: for F being semi-continuous PGraphMapping of G1,G2 st F _V is PVertexMapping of G1,G2 & ( 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 e9 being object st
( e9 in rng (F _E) & e9 Joins (F _V) . v,(F _V) . w,G2 ) ) holds
F _V is continuous PVertexMapping of G1,G2
let F be semi-continuous PGraphMapping of G1,G2; :: thesis: ( F _V is PVertexMapping of G1,G2 & ( 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 e9 being object st
( e9 in rng (F _E) & e9 Joins (F _V) . v,(F _V) . w,G2 ) ) implies F _V is continuous PVertexMapping of G1,G2 )
assume that
A1: F _V is PVertexMapping of G1,G2 and
A2: 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 e9 being object st
( e9 in rng (F _E) & e9 Joins (F _V) . v,(F _V) . w,G2 ) ; :: thesis: F _V is continuous PVertexMapping of G1,G2
reconsider f = F _V as PVertexMapping of G1,G2 by A1;

now :: thesis: for v, w, e9 being object st v in dom f & w in dom f & e9 Joins f . v,f . w,G2 holds
ex e being object st e Joins v,w,G1

let v, w, e9 be object ; :: thesis: ( v in dom f & w in dom f & e9 Joins f . v,f . w,G2 implies ex e being object st e Joins v,w,G1 )
assume A3: ( v in dom f & w in dom f & e9 Joins f . v,f . w,G2 ) ; :: thesis: ex e being object st e Joins v,w,G1
then e9 Joins f /. v,f . w,G2 by PARTFUN1:def 6;
then e9 Joins f /. v,f /. w,G2 by A3, PARTFUN1:def 6;
then consider e8 being object such that
A4: ( e8 in rng (F _E) & e8 Joins f . v,f . w,G2 ) by A2, A3, CHORD:def 3;
consider e being object such that
A5: ( e in dom (F _E) & (F _E) . e = e8 ) by A4, FUNCT_1:def 3;
take e = e; :: thesis: e Joins v,w,G1
thus e Joins v,w,G1 by A3, A4, A5, GLIB_010:def 15; :: thesis: verum

end;

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