for x being ExtReal holds
( x = 0 iff |.x.| = 0 ) by Th4, Def1;