Add geo2sum to iset.mm
Add geo2sum to iset.mm

Stated as in set.mm.  The proof is essentially the set.mm one.  Although
many steps need a bit of intuitionizing, nothing had to change very
much.

metamath/set.mm,metamath/set.mm,metamath/set.mm