take ArProg (0,1) ; :: thesis: ( ArProg (0,1) is increasing & ArProg (0,1) is non-decreasing )
thus ( ArProg (0,1) is increasing & ArProg (0,1) is non-decreasing ) ; :: thesis: verum