theorem :: TOPGEN_3:24

for r being Real
for X being set st 0 < r & r < 1 holds
Sum (X -powers r) <= Sum (r GeoSeq)