instance PiBase.instCountableChainConditionOfSeparableSpace {X : Type u} [TopologicalSpace X] [h : TopologicalSpace.SeparableSpace X] : CountableChainCondition X

Theorem T21: P26 (SeparableSpace) => P29 (CountableChainCondition)

theorem PiBase.Formal.T21 : P26 ≤ P29