:: deftheorem defines op1 ANPROJ10:def 2 :
for r being non zero non unit Real holds op1 r = 1 / r;