Positive real step function

Set

 context $\langle X,\Sigma\rangle\in\mathrm{MeasurableSpace}(X)$
 postulate $f\in \mathcal T^+$
 context $f\in \mathcal T$ context …Real step function
 $x\in X$
 postulate $f(x)\ge 0$