Disjoint uses ⊥ (U+22A5 -- UP TACK) but should use ⟂ (U+27C2 -- PERPENDICULAR)

The issue here is that I can no longer use ⊥ for the bottom element of a lattice.

Of course, we can decide to swap the two similarly looking symbols, but this is not particularly clean.

Changing the symbols will create some incompatibility issues, but these can be easily fixed using a sed script or so.