:: deftheorem Def01 defines unit ANPROJ10:def 1 :
for r being Real holds
( r is unit iff r = 1 );