:: deftheorem defines ||.. INTEGRA9:def 3 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL holds ||..f,A..|| = sqrt |||(f,f,A)|||;