take bool X ; :: thesis: ( bool X is non-decreasing-closed & bool X is non-increasing-closed )
thus ( bool X is non-decreasing-closed & bool X is non-increasing-closed ) ; :: thesis: verum