for G1, G2 being _Graph
for H being Subgraph of G1
for F being PGraphMapping of G1,G2 holds
( ( F is empty implies F | H is empty ) & ( F is total implies F | H is total ) & ( F is one-to-one implies F | H is one-to-one ) & ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) & ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )