:: deftheorem defines nonnegative RINFSUP1:def 3 :
for f being Real_Sequence holds
( f is nonnegative iff for n being Nat holds f . n >= 0 );