The category of posets without isolated points

[ScriptRaccoon]

This PR adds the category of posets without isolated points. It provides an example of an infinitary extensive category that is not Cauchy complete.

This PR contributes to the milestone of reducing the number of unwitnessed yet consistent property combinations.

The result multi-complete => Cauchy complete is also added. This makes some previous proofs redundant.

New combinations

Found 17 unique witnessed combinations by the supplied structures (Pos_noiso):

Directly witnessed:
- countably extensive ∧ ¬Cauchy complete
- countably extensive ∧ ¬multi-terminal object
- countably extensive ∧ ¬natural numbers object
- countably extensive ∧ ¬terminal object
- disjoint coproducts ∧ ¬natural numbers object
- extensive ∧ ¬Cauchy complete
- infinitary extensive ∧ ¬Cauchy complete
- infinitary extensive ∧ ¬multi-terminal object
- infinitary extensive ∧ ¬natural numbers object
- infinitary extensive ∧ ¬terminal object

Dually witnessed:
- countably coextensive ∧ ¬Cauchy complete
- countably coextensive ∧ ¬multi-initial object
- countably coextensive ∧ ¬initial object
- coextensive ∧ ¬Cauchy complete
- infinitary coextensive ∧ ¬Cauchy complete
- infinitary coextensive ∧ ¬multi-initial object
- infinitary coextensive ∧ ¬initial object

The number of unwitnessed combinations went down from 687 to 668. (The 2 extra are multi-complete ∧ ¬ Cauchy complete and its dual, which are not consistent anymore.)