 The foregoing work on \(\textrm{CH}\) can be formalised in  CZF,  which is equiconsistent with classical Zermelo–Fraenkel set theory,  ZF.  If we allow ourselves to invoke the Gödel–Cohen theorem that the Continuum Hypothesis is independent of ZF, then we can draw some interesting conclusions by looking more closely at our proof that \(\textrm{CH}\) implies LEM. To do so, take \(p=\textrm{CH}\) in our proof, so that  \[ X≡ \{S \in \textrm{dch}(\bN) : \textrm {CH} \vee \neg \textrm{CH} \}. \]  If \(X=0\), then \(\neg (\textrm{CH} \vee \neg \textrm{CH})\), which is absurd; so \(\neg(X=0)\). On the other hand, if \(X\) is inhabited — that is, contains a point — then \(\textrm{CH} \vee \neg \textrm{CH}\), so under the constructive interpretation of '\(\vee\)', either we have a proof of \(\textrm{CH}\) or else we have a proof of \(\neg \textrm{CH}\). Since this runs counter to the aforementioned Gödel–Cohen theorem, we may regard \(X\) as an explicit example of a set that is not empty but for which it is impossible to construct a member. This, in itself, is not uninteresting; but it also gives a new insight into the constructive status of \(\textrm{CH}\). From our proof that \(\textrm{CH}\) implies LEM we see that the set \(C≡\bN \cup X\) satisfies  \[     \bN≲C≲\textrm{dch}(\bN) \wedge \neg(C \cong \bN).     \]  Also,  \[     \neg(C \cong \textrm{dch}(\bN)) \Rightarrow X=0,     \]  which is absurd, so \(\neg\neg(C \cong \textrm{dch}(\bN))\). On the other hand,  \[ C \cong \textrm{dch}(\bN) \Rightarrow \textrm{CH} \vee \neg \textrm{CH}. \]  Thus, provided \(\textrm{CH}\) is independent of CZF (which, in view of equiconsistency of CZF and ZF, it had better be), we see that \(C\) is an explicit example of a set that has the property  \[     \bN≲C≲\textrm{dch}(\bN) \wedge \neg(C\cong \bN) \wedge \neg \neg (C \cong \textrm{dch}(\bN))     \]  but, within CZF, cannot be proved equinumerous with \(\textrm{dch}(\bN)\). 