:: deftheorem defines Cst INTEGRA8:def 1 :
for r being Real holds Cst r = REAL --> r;