 Call the system that results from adding this formula to our current system “KTd”. The addition of T makes derivable our previously mentioned axiom \(\OB\)-U of SDL+, which we have shown is not derivable in SDL  itself:[39]