Доказательство в книге Джонстона для локалей
действительно занудное, но я подозреваю, что это
из-за того, что Джонстон не развивает нормально
общую топологию, а доказывает отдельные нужные ему факты.

Учить первокурсников локалям затруднительно ввиду
отсутствия учебника общей топологии на языке локалей.
Впрочем, тогда надо и функциональный анализ, теорию меры,
алгебраическую геометрию на локали
переводить — таких учебников тоже ещё нет.

То есть сначала нужен новый Бурбаки, который догматично
заменит топологические пространства локалями,
напишет книги на этом языке,
а потом уже можно начинать писать учебники и учить студентов.

Я бы всё-таки не стал называть классические топологические
пространства «нормальной» топологией — ведь именно этот формализм
принуждает нас к теоретико-множественным извращениям
и не позволяет нормально доказывать семейственные и эквивариантные
версии теорем из общей топологии.
Термин «классическая общая топология» мне кажется более уместным.