theorem :: EXTREAL1:3

for x being R_eal st 0 <= x holds
|.x.| = x by Def1;