theorem Th17: :: BINARI_2:17

for m being non zero Nat
for x, y being Tuple of m, BOOLEAN holds x - y = x + (Neg2 y)