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

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