for G1, G2 being _Graph
for G being GraphUnion of G1,G2 st G1 tolerates G2 & the_Edges_of G1 misses the_Edges_of G2 holds
G .size() = (G1 .size()) +` (G2 .size())