theorem :: ORDERS_5:48

for A being Preorder
for f being finite-support Function of A,REAL st f is nonpositive-yielding holds
eqSumOf f is nonpositive-yielding