theorem :: GLIB_015:130

for G1, G2 being _Graph
for S being GraphSum of G1,G2 holds S .size() = (G1 .size()) +` (G2 .size())