Add geo2sum2 to iset.mm
Add geo2sum2 to iset.mm

Stated as in set.mm.  The proof is the set.mm one, intuitionized in a
few places but without needing a lot of changes.

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