Part 4 of completing S110

[david20000813]

Continuing #1128, #1129, and #1130, this is the fourth and final PR in a series to complete the traits of S110, the strong ultrafilter topology. This one added the three remaining traits: P32 (Countably paracompact), P33 (Countably metacompact), and P194 (Submetacompact). In addition, I've included a proof for P22 (Pseudocompact), which was originally just "asserted in the general reference chart" of Counterexamples.

This PR got delayed a bit, mostly because I was waiting the earlier three parts to be approved so that, in the final part, I can check to make sure there is no redundant trait. (And then because of the holidays.) There is indeed none.

[prabau]

I reviewed Countably metacompact (P33) and Submetacompact (P194). No problem for those.

I'll leave the other two to someone more knowledgeable.

[yhx-12243]

{S110|P33} will become redundant due to #1204.

[StevenClontz]

Marking as blocked pending #1285