theorem :: BASEL_1:34
( lim Basel-seq1 = (PI ^2) / 6 & (PI ^2) / 6 = lim Basel-seq2 )