Completely prime filter
= 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.