set f = - seq;
Partial_Sums (- seq) is nonnegative ;
then - (Partial_Sums seq) is nonnegative by Th1;
then - (- (Partial_Sums seq)) is nonpositive ;
hence Partial_Sums seq is nonpositive by Th2; :: thesis: verum