:: deftheorem Def100 defines ExAbsval BINARI_6:def 6 :
for x being Element of BOOLEAN *
for b₂ being Nat holds
( b₂ = ExAbsval x iff ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & b₂ = Absval y ) );