:: deftheorem defines x_r-seq BASEL_1:def 5 :
for m being Nat holds x_r-seq m = (PI / ((2 * m) + 1)) (#) (idseq m);