instance PiBase.instKcSpaceOfStronglyKcSpace {X : Type u} [TopologicalSpace X] [h : StronglyKcSpace X] : KcSpace X

Theorem T234: P103 (StronglyKcSpace) => P100 (KcSpace)

theorem PiBase.Formal.T234 : P103 ≤ P100