Totally connected locale
= Totally connected locale
A positive <open locale> is totally connected when every <positive open of a locale> is connected. Under classical logic its positive opens form a <completely prime filter>, hence specify a dense point. Positivity of the whole locale is essential: the empty locale satisfies the condition on positive opens vacuously but has no point.