take cobool X ; :: thesis: cobool X is diff-finite-partition-closed
thus cobool X is diff-finite-partition-closed ; :: thesis: verum