Syntax definition csumge0

Description: Extend class notation to include the sum of nonnegative extended reals.

	Ref	Expression
Assertion	csumge0	$$class\mathrm{sum^}$$