Syntax definition csumge0

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

	Ref	Expression
Assertion	csumge0	class sum^