Description: Property P000016 of pi-base. The class of compact topologies. A space X is compact if every open cover of X has a finite subcover. This theorem is just a relabelled copy of iscmp . (Contributed by ML, 8-Dec-2020)