let G1, G2 be _Graph; :: thesis: [{},{}] is empty one-to-one Dcontinuous PGraphMapping of G1,G2
reconsider F = [{},{}] as PGraphMapping of G1,G2 by Lm3;
A1: F is empty ;
thus [{},{}] is empty one-to-one Dcontinuous PGraphMapping of G1,G2 by A1; :: thesis: verum