theorem :: SERIES_1:33

for p being Real
for s being Real_Sequence st p <= 1 & ( for n being Nat st n >= 1 holds
s . n = 1 / (n to_power p) ) holds
not s is summable