Description: The propositional function ( ch -> ( . -> th ) ) is decreasing. (Contributed by BJ, 19-Jul-2019)