:: deftheorem defines zeroCCoset LPSPACC1:def 17 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds zeroCCoset M = a.e-Ceq-class ((X --> 0c),M);