:: deftheorem Def6 defines - BINARI_2:def 6 :
for n being non zero Nat
for x, y, b₄ being Tuple of n, BOOLEAN holds
( b₄ = x - y iff for i being Nat st i in Seg n holds
b₄ /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry (x,(Neg2 y))) /. i) );