let G1, G2 be non-Dmulti _Graph; :: thesis: for f being directed PVertexMapping of G1,G2 st f is one-to-one holds
( DPVM2PGM f is semi-Dcontinuous & DPVM2PGM f is semi-continuous )
let f be directed PVertexMapping of G1,G2; :: thesis: ( f is one-to-one implies ( DPVM2PGM f is semi-Dcontinuous & DPVM2PGM f is semi-continuous ) )
assume f is one-to-one ; :: thesis: ( DPVM2PGM f is semi-Dcontinuous & DPVM2PGM f is semi-continuous )
then DPVM2PGM f is one-to-one by Th35;
hence ( DPVM2PGM f is semi-Dcontinuous & DPVM2PGM f is semi-continuous ) ; :: thesis: verum