Eliminating disjunctions by disjunction elimination

Applications include syntactical counterparts of the theorems or lemmas known under the names of Artin-Schreier, Krull-Lindenbaum and Szpilrajn, as well as of the spatiality of coherent locales. Related work has been done before on individual instances, e.g. in locale theory, dynamical algebra, formal topology and proof analysis.