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