 In its classical contrapositive form, FT\(_D\) is known as König’s Lemma: if for every \(n\) there exists a path of length \(n\) that misses \(B\), then there exists an infinite path that misses \(B\) (see Dummett 1977 [2000], 49–53). (Of course, classically the condition of detachability is superfluous.) It is simple to construct a Brouwerian counterexample to König’s Lemma.