theorem :: BASEL_1:30

for m being Nat holds Sum ((sqr (x_r-seq m)) ") <= Sum (sqr (cosec (x_r-seq m)))