 Connected locale

Under classical logic a positive locale is connected when it cannot be written as the union of two disjoint nonzero opens. Equivalently its only complemented opens are $0$ and $1$. An open sublocale uses this criterion relative to its own top element. Positivity of the whole locale excludes the empty locale. This definition is stated with its logical convention; replacing positivity by negated nonemptiness is not a constructive step.