There is a <a href=../basicNotions.html>topology T</a>:
<dl>
<dt>x⊂y ≜ ∀z (z∊x → z∊y)<dd>(x is included in y)
<dt>Cx ≜ x⊂T ∧ ∀y(y∊T → ∃z(y∊z∧z∊x))<dd>(x is an open cover of T)
<dt>Rxy ≜ Cx ∧ Cy ∧ ∀z(z∊x → ∃w(w∊y ∧ z⊂y))<dd>(x is a refinement of y)
<dt>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))))
<dd>(The dimension of T is less than 3)
<dt>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))))
<dd>(The dimension of T is less than 2)
<dt>D2 ≜ L3∧¬L2<dd>(T is 2 dimensional)
</dl>

¬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))))