theorem :: TOPREALC:18

for r being Real holds |.<*r*>.| = |.r.|