|x|=a ⇔ ((x<0)→(x=-a))∧(x>0)→(x=a))
|x|=a → (x=-a)∨(x=a)