let G1, G2 be non-multi _Graph; :: thesis: for f being PVertexMapping of G1,G2 st f is continuous & f is one-to-one holds
PVM2PGM f is semi-continuous
let f be PVertexMapping of G1,G2; :: thesis: ( f is continuous & f is one-to-one implies PVM2PGM f is semi-continuous )
assume A1: ( f is continuous & f is one-to-one ) ; :: thesis: PVM2PGM f is semi-continuous
set g = (PVM2PGM f) _E ;

now :: thesis: for e, v, w being object st e in dom ((PVM2PGM f) _E) & v in dom ((PVM2PGM f) _V) & w in dom ((PVM2PGM f) _V) & ((PVM2PGM f) _E) . e Joins ((PVM2PGM f) _V) . v,((PVM2PGM f) _V) . w,G2 holds
e Joins v,w,G1

let e, v, w be object ; :: thesis: ( e in dom ((PVM2PGM f) _E) & v in dom ((PVM2PGM f) _V) & w in dom ((PVM2PGM f) _V) & ((PVM2PGM f) _E) . e Joins ((PVM2PGM f) _V) . v,((PVM2PGM f) _V) . w,G2 implies e Joins v,w,G1 )
assume A2: ( e in dom ((PVM2PGM f) _E) & v in dom ((PVM2PGM f) _V) & w in dom ((PVM2PGM f) _V) ) ; :: thesis: ( ((PVM2PGM f) _E) . e Joins ((PVM2PGM f) _V) . v,((PVM2PGM f) _V) . w,G2 implies e Joins v,w,G1 )
assume A3: ((PVM2PGM f) _E) . e Joins ((PVM2PGM f) _V) . v,((PVM2PGM f) _V) . w,G2 ; :: thesis: e Joins v,w,G1
then ((PVM2PGM f) _E) . e Joins f . v,f . w,G2 ;
then consider e0 being object such that
A4: e0 Joins v,w,G1 by A1, A2, Th2;
e0 in G1 .edgesBetween (dom f) by A2, A4, GLIB_000:32;
then A5: e0 in dom ((PVM2PGM f) _E) by Def10;
then ((PVM2PGM f) _E) . e0 Joins ((PVM2PGM f) _V) . v,((PVM2PGM f) _V) . w,G2 by A2, A4, GLIB_010:4;
then A6: ((PVM2PGM f) _E) . e0 = ((PVM2PGM f) _E) . e by A3, GLIB_000:def 20;
PVM2PGM f is one-to-one by A1, Th34;
hence e Joins v,w,G1 by A2, A4, A5, A6, FUNCT_1:def 4; :: thesis: verum

end;

hence PVM2PGM f is semi-continuous by GLIB_010:def 15; :: thesis: verum