theorem :: HAHNBAN1:9

for r being Real holds |.[**r,0**].| = |.r.| ;