:: deftheorem defines 'not' BINARITH:def 1 :
for n being Nat
for x, b₃ being Tuple of n, BOOLEAN holds
( b₃ = 'not' x iff for i being Nat st i in Seg n holds
b₃ /. i = 'not' (x /. i) );