There is a topology T:
- x⊂y ≜ ∀z (z∊x → z∊y)
- (x is included in y)
- Cx ≜ x⊂T ∧ ∀y(y∊T → ∃z(y∊z∧z∊x))
- (x is an open cover of T)
- Rxy ≜ Cx ∧ Cy ∧ ∀z(z∊x → ∃w(w∊y ∧ z⊂y))
- (x is a refinement of y)
- L3 ≜ ∀x(Cx → ∃y(Ryx ∧ ∀z(z∊T → ∀a∀b∀c∀d(a∊y∧b∊y∧c∊y∧d∊y∧z∊a∧z∊b∧z∊c∧z∊d → a=b∨a=c∨a=d∨b=c∨b=d∨c=d))))
- (The dimension of T is less than 3)
- L2 ≜ ∀x(Cx → ∃y(Ryx ∧ ∀z(z∊T → ∀a∀b∀c(a∊y∧b∊y∧c∊y∧z∊a∧z∊b∧z∊c → a=b∨a=c∨b=c))))
- (The dimension of T is less than 2)
- D2 ≜ L3∧¬L2
- (T is 2 dimensional)

¬L2 = ∃x(Cx ∧ ∃y(Ryx ∧ ∀z(z∊T → ∀a∀b∀c(a∊y∧b∊y∧c∊y∧z∊a∧z∊b∧z∊c → a=b∨a=c∨b=c))))