theorem :: EXTREAL1:13

for x being ExtReal holds
( |.x.| = x or |.x.| = - x ) by Def1;