:: deftheorem defines Basel-seq2 BASEL_1:def 8 :
Basel-seq2 = (((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,2,2,1));