:: deftheorem Def3 defines Intval BINARI_2:def 3 :
for n being Nat
for x being Tuple of n, BOOLEAN holds
( ( x /. n = FALSE implies Intval x = Absval x ) & ( not x /. n = FALSE implies Intval x = (Absval x) - (2 to_power n) ) );