DPRM_Theorem.Binary_And