theorem Th17: :: MESFUN12:17

for X being set
for A being Subset of X
for er being ExtReal holds
( ( er >= 0 implies chi (er,A,X) is nonnegative ) & ( er <= 0 implies chi (er,A,X) is nonpositive ) )