theorem Th17: :: DESCIP_1:17

for n being non zero Element of NAT
for s, t being Element of n -tuples_on BOOLEAN holds Op-XOR ((Op-XOR (s,t)),t) = s