for n being Nat holds
( Basel-seq1 . n <= (Partial_Sums Basel-seq) . n & (Partial_Sums Basel-seq) . n <= Basel-seq2 . n )

proof

let n be Nat; :: thesis: ( Basel-seq1 . n <= (Partial_Sums Basel-seq) . n & (Partial_Sums Basel-seq) . n <= Basel-seq2 . n )
Sum (Basel-seq,n) = Sum (Basel-seq,n) ;
hence ( Basel-seq1 . n <= (Partial_Sums Basel-seq) . n & (Partial_Sums Basel-seq) . n <= Basel-seq2 . n ) by Th30, Th31; :: thesis: verum

end;

hence Sum Basel-seq = (PI ^2) / 6 by SEQ_2:20, BASEL_1:34; :: thesis: verum