:: deftheorem Def10 defines OS_Meas MEASURE7:def 10 :
for b₁ being Function of (bool REAL),ExtREAL holds
( b₁ = OS_Meas iff for A being Subset of REAL holds b₁ . A = inf (Svc A) );