let G1, G2 be non-multi _Graph; :: thesis: for f being PVertexMapping of G1,G2 st f is total & f is one-to-one holds
PVM2PGM f is weak_SG-embedding
let f be PVertexMapping of G1,G2; :: thesis: ( f is total & f is one-to-one implies PVM2PGM f is weak_SG-embedding )
assume ( f is total & f is one-to-one ) ; :: thesis: PVM2PGM f is weak_SG-embedding
then ( PVM2PGM f is total & PVM2PGM f is one-to-one ) by Th32, Th34;
hence PVM2PGM f is weak_SG-embedding ; :: thesis: verum