:: deftheorem Def2 defines absreal EUCLID:def 2 :
for b₁ being Function of REAL,REAL holds
( b₁ = absreal iff for r being Real holds b₁ . r = |.r.| );