instance PiBase.instCollectionwiseNormalSpaceOfHereditarilyCollectionwiseNormalSpace {X : Type u} [TopologicalSpace X] [h : HereditarilyCollectionwiseNormalSpace X] : CollectionwiseNormalSpace X

Theorem T665: P108 (HereditarilyCollectionwiseNormalSpace) => P88 (CollectionwiseNormalSpace)

theorem PiBase.Formal.T665 : P108 ≤ P88