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