:: deftheorem defines Inv MEASURE6:def 8 :
for X being Subset of REAL holds Inv X = { (1 / r3) where r3 is Real : r3 in X } ;