 Completely prime filter

An upward-closed subset of a frame containing $1$, excluding $0$ and closed under finite meets is completely prime if membership of an arbitrary join implies membership of some summand. Its characteristic map is a point of a frame. Constructively the map takes values in the frame of truth values.