:: deftheorem defines COMPLEX MEASURE7:def 9 :
for A being Subset of REAL holds COMPLEX A = inf (Svc A);