theorem :: DESCIP_1:32

for message, secretkey being Element of 64 -tuples_on BOOLEAN holds DES-DEC ((DES-ENC (message,secretkey)),secretkey) = message by Th31;