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