:: deftheorem defines Neg2 BINARI_2:def 2 :
for n being non zero Nat
for x being Tuple of n, BOOLEAN holds Neg2 x = ('not' x) + (Bin1 n);