reconsider F = [{},{}] as PGraphMapping of G1,G2 by Lm3;
take
F
; ( 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 )
; verum