let n be Nat; :: thesis: Basel-seq . n >= 0
Basel-seq . n = 1 / (n ^2) by BASEL_1:31;
hence Basel-seq . n >= 0 ; :: thesis: verum