reconsider F = [{},{}] as PGraphMapping of G1,G2 by Lm3;

take F ; :: thesis: ( F is empty & F is one-to-one & F is Dcontinuous & F is directed & F is continuous & F is semi-Dcontinuous & F is semi-continuous )

thus ( F is empty & F is one-to-one & F is Dcontinuous & F is directed & F is continuous & F is semi-Dcontinuous & F is semi-continuous ) ; :: thesis: verum

take F ; :: thesis: ( F is empty & F is one-to-one & F is Dcontinuous & F is directed & F is continuous & F is semi-Dcontinuous & F is semi-continuous )

thus ( F is empty & F is one-to-one & F is Dcontinuous & F is directed & F is continuous & F is semi-Dcontinuous & F is semi-continuous ) ; :: thesis: verum