instance PiBase.instSeparableSpaceOfHereditarilySeparableSpace {X : Type u} [TopologicalSpace X] [h : HereditarilySeparableSpace X] : TopologicalSpace.SeparableSpace X

Theorem T440: P180 (HereditarilySeparableSpace) => P26 (SeparableSpace)

theorem PiBase.Formal.T440 : P180 ≤ P26