theorem :: DESCIP_1:28

DES-PIPINV = DES-PIP " by Lm7, FUNCT_2:60;