take binop D ; :: thesis: ( binop D is associative & binop D is commutative )
thus ( binop D is associative & binop D is commutative ) ; :: thesis: verum