  is assertable. But it follows from (1) that we may assert \(A \rightarrow U ≈ V\), and so also, using the Extensionality of Functions, \(A \rightarrow KU = KV\). This yields the assertability of \(KU \ne KV \rightarrow  \neg A\), which, together with (3) in turn yields the assertability of