theorem Th16: :: MEASURE7:16

OS_Meas is C_Measure of REAL